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

chore(tests/lean/run/group3): cleanup test

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-03 09:20:49 -07:00
parent 7ea9c32ec8
commit fd013e8d07
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/run/group3.lean
View file

@ -41,8 +41,9 @@ mk : Π mul: A → A → A,
namespace semigroup namespace semigroup
section section
parameters {A : Type} {s : semigroup A} parameters {A : Type} {s : semigroup A}
definition mul (a b : A) : A := semigroup.rec (λmul assoc, mul) s a b variables a b c : A
definition assoc {a b c : A} : mul (mul a b) c = mul a (mul b c) := definition mul := semigroup.rec (λmul assoc, mul) s a b
definition assoc : mul (mul a b) c = mul a (mul b c) :=
semigroup.rec (λmul assoc, assoc) s a b c semigroup.rec (λmul assoc, assoc) s a b c
end end
end semigroup end semigroup
@ -53,7 +54,7 @@ section
definition semigroup_has_mul [instance] : has_mul A := has_mul.mk (semigroup.mul) definition semigroup_has_mul [instance] : has_mul A := has_mul.mk (semigroup.mul)
theorem mul_assoc [instance] (a b c : A) : a * b * c = a * (b * c) := theorem mul_assoc [instance] (a b c : A) : a * b * c = a * (b * c) :=
semigroup.assoc !semigroup.assoc
end end