michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/run/elim2): adjust test to reflect recent changes

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-05 10:54:00 -08:00
parent d6958be7e7
commit 1b73764ad3
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/run/elim2.lean
View file

@ -4,5 +4,5 @@ constant p : num → num → num → Prop
axiom H1 : ∃ x y z, p x y z axiom H1 : ∃ x y z, p x y z
axiom H2 : ∀ {x y z : num}, p x y z → p x x x axiom H2 : ∀ {x y z : num}, p x y z → p x x x
theorem tst : ∃ x, p x x x theorem tst : ∃ x, p x x x
:= obtain a b c H [visible], from H1, := obtain a b c H, from H1,
by (apply exists.intro; apply H2; eassumption) by (apply exists.intro; apply H2; eassumption)