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

fix(tests/lean): adjust tests to reflect modifications in the pp

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-27 18:38:45 -08:00
parent abc370a011
commit 8e86d6578c
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/exists4.lean.expected.out
View file

@ -15,7 +15,7 @@ Theorem T1 : ∃ x y z : N, P x y z :=
N
(λ x : N, ∃ y z : N, P x y z)
a
(@ExistsIntro N (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1) b (@ExistsIntro N (λ z : N, P a b z) c H3))
(@ExistsIntro N (λ x : N, ¬ (∀ x::1 : N, ¬ P a x x::1)) b (@ExistsIntro N (λ z : N, P a b z) c H3))
Theorem T2 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))
Theorem T3 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))
Theorem T4 (H : P a a b) : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro a (ExistsIntro b H))