From 70066eaea73a22383e18bb8cdfc1d5cadbbe0afe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 16 Jul 2019 10:53:00 -0700 Subject: [PATCH] chore(library/init/wf): add parentheses --- library/init/wf.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/wf.lean b/library/init/wf.lean index 7600de998d..a2fef9d380 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -54,7 +54,7 @@ theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, r y x → C y) recursion hwf a h variable {C : α → Sort v} -variable F : ∀ x, (∀ y, r y x → C y) → C x +variable (F : ∀ x, (∀ y, r y x → C y) → C x) def fixF (x : α) (a : Acc r x) : C x := Acc.recOn a (fun x₁ ac₁ ih => F x₁ ih)