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

fix(tests/lean): update expected result to reflect recent changes

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-06 16:31:13 -08:00
parent 015bff8283
commit daadff548e
2 changed files with 2 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/tactic2.lean.expected.out
View file

@ -10,9 +10,4 @@ Theorem T2 : p ⇒ q ⇒ p ∧ q ∧ p := Discharge (λ H : p, Discharge (λ H::
Theorem T3 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
Discharge
(λ H : p,
Discharge
(λ H::1 : p ∧ q,
Discharge
(λ H::2 : r,
Conj (let H::1::2 := Conjunct2 H::1 in H::1::2)
(Conj H::2 (let H::1::1 := Conjunct1 H::1 in H::1::1)))))
Discharge (λ H::1 : p ∧ q, Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (Conj H::2 (Conjunct1 H::1)))))

7
tests/lean/tactic3.lean.expected.out
View file

@ -7,9 +7,4 @@
Theorem T1 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
Discharge
(λ H : p,
Discharge
(λ H::1 : p ∧ q,
Discharge
(λ H::2 : r,
Conj (let H::1::2 := Conjunct2 H::1 in H::1::2)
(Conj H::2 (let H::1::1 := Conjunct1 H::1 in H::1::1)))))
Discharge (λ H::1 : p ∧ q, Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (Conj H::2 (Conjunct1 H::1)))))