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

test(tests/lean/run): add test showing that "proof ... qed" can access the whole context

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-05 18:32:21 -07:00
parent 7aa0e466a5
commit 5d515a06f7
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/proof_qed_improved.lean Normal file
View file

@ -0,0 +1,6 @@
example (a b c : nat) (f : nat → nat → nat) (H₁ : a = b) (H₂ : b = c) : f (f a a) (f b b) = f (f c c) (f c c) :=
have h : a = c, from eq.trans H₁ H₂,
proof
calc f (f a a) (f b b) = f (f c c) (f b b) : by rewrite h
... = f (f c c) (f c c) : by rewrite H₂
qed