From 9dcd95df2f61386847d64be071d3e8f6641a5474 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sat, 15 Jul 2017 21:13:33 +0100 Subject: [PATCH] chore(tests/lean/anc1): fix tests --- tests/lean/anc1.lean.expected.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out index 9326c24d80..396e79cb0f 100644 --- a/tests/lean/anc1.lean.expected.out +++ b/tests/lean/anc1.lean.expected.out @@ -3,7 +3,7 @@ and.intro trivial trivial : true ∧ true anc1.lean:5:0: warning: declaration '[anonymous]' uses sorry ⟨1, sorry⟩ : Σ' (x : ℕ), x > 0 show true, from true.intro : true -Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0 +Exists.intro 1 (id_locked (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from and.intro Hb Ha : ∀ (A B C : Prop), A → B → C → B ∧ A λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C),