max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test(tests/lean/elab10): test show/have-exprs using new elaborator

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-27 16:50:18 -07:00
parent 084f82b00b
commit 4fd69ca2d4
2 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
tests/lean/elab10.lean
View file

@ -13,3 +13,8 @@ attribute int_comm_ring [instance]
#elab int → int
#elab ((λ x, x + 1) : int → int)
#elab λ (A : Type) (a b c d : A) (H1 : a = b) (H2 : b = c) (H3 : d = c),
have a = c, from eq.trans H1 H2,
have H3' : c = d, from eq.symm H3,
show a = d, from eq.trans this H3'

5
tests/lean/elab10.lean.expected.out
View file

@ -7,3 +7,8 @@ int → int : Type
@add int (@distrib.to_has_add int (@ring.to_distrib int (@comm_ring.to_ring int int_comm_ring))) x
(@one int (@monoid.to_has_one int (@ring.to_monoid int (@comm_ring.to_ring int int_comm_ring)))) :
int → int
λ (A : Type) (a b c d : A) (H1 : @eq A a b) (H2 : @eq A b c) (H3 : @eq A d c),
have this : @eq A a c, from @eq.trans A a b c H1 H2,
have H3' : @eq A c d, from @eq.symm A d c H3,
show @eq A a d, from @eq.trans A a c d this H3' :
∀ (A : Type) (a b c d : A), @eq A a b → @eq A b c → @eq A d c → @eq A a d