From 2368b4097c34faf36cec4dc2ebbd0eb80f4bc52d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Jan 2014 12:36:10 -0800 Subject: [PATCH] fix(examples/lean): typo Signed-off-by: Leonardo de Moura --- examples/lean/wf.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/lean/wf.lean b/examples/lean/wf.lean index b6121354a..ee157ed91 100644 --- a/examples/lean/wf.lean +++ b/examples/lean/wf.lean @@ -11,7 +11,7 @@ theorem wf_induction {A : (Type U)} {R : A → A → Bool} {P : A → Bool} (Hwf : ∀ x, P x := refute (λ N : ¬ ∀ x, P x, obtain (w : A) (Hw : ¬ P w), from not_forall_elim N, - -- The main "trick" is to define Q x and ¬ P x. + -- The main "trick" is to define Q x as ¬ P x. -- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬ P r) let Q : A → Bool := λ x, ¬ P x, Qw : ∃ w, Q w := exists_intro w Hw,