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

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

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-19 18:00:14 -08:00
parent dfbe6662be
commit 6fd0d452d3
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/run/group4.lean
View file

@ -128,12 +128,12 @@ test1 a b c d
theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
calc
a * 1 * b * c = a * b * c : mul_right_id
a * 1 * b * c = a * b * c : {!mul_right_id}
... = a * (b * c) : mul_assoc
theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
calc
a * 1 * b * c = a * b * c : mul_right_id
a * 1 * b * c = a * b * c : {!mul_right_id}
... = a * (b * c) : mul_assoc
theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) :=

2
tests/lean/run/nested_rec.lean
View file

@ -29,7 +29,7 @@ theorem g_succ (a : nat) : g (succ a) = g (g a) :=
have aux : well_founded.fix g.F (succ a) = sigma.mk (g (g a)) _, from
well_founded.fix_eq g.F (succ a),
calc g (succ a) = pr₁ (well_founded.fix g.F (succ a)) : rfl
... = pr₁ (sigma.mk (g (g a)) _) : aux
... = pr₁ (sigma.mk (g (g a)) _) : {aux}
... = g (g a) : rfl
theorem g_all_zero (a : nat) : g a = zero :=