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

test(tests/lean/run/class5): improve test

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-13 22:39:16 +01:00
parent bdfd219246
commit e432e23115
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -26,6 +26,7 @@ section
using algebra nat
variables a b c : nat
check a * b * c
definition tst1 : nat := a * b * c
end
section
@ -34,6 +35,7 @@ section
-- check mul_struct nat << This is an error, we are using only the notation from algebra
variables a b c : nat
check a * b * c
definition tst2 : nat := a * b * c
end
section
@ -41,15 +43,16 @@ section
-- check mul_struct nat << This is an error, we are using only the notation from algebra
variables a b c : nat
check #algebra a*b*c
definition tst3 : nat := #algebra a*b*c
end
section
using nat
set_option pp.implicit true
definition add_struct [instance] : algebra.mul_struct nat
:= algebra.mk_mul_struct add
variables a b c : nat
check #algebra a*b*c -- << is using add instead of mul
definition tst4 : nat := #algebra a*b*c
end