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

test(tests/lean/run): add rewrite tactic test

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-06 14:14:42 -08:00
parent 5b25da8c43
commit 04f8278c90
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
tests/lean/run/rewriter16.lean Normal file
View file

@ -0,0 +1,8 @@
import data.nat
open nat
theorem tst (x : nat) (H1 : x = 0) : x = 0 :=
begin
rewrite *add_zero,
rewrite H1
end