max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/lean/anc1): fix tests

Browse source
This commit is contained in:
Gabriel Ebner 2017-07-15 21:13:33 +01:00
parent 563c1bcffe
commit 9dcd95df2f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/anc1.lean.expected.out
View file

@ -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),