test(tests/lean/run): add more rewrite tactic tests
This commit is contained in:
parent
979d6494e9
commit
78bde6c9e6
2 changed files with 19 additions and 0 deletions
7
tests/lean/run/rewriter13.lean
Normal file
7
tests/lean/run/rewriter13.lean
Normal file
|
@ -0,0 +1,7 @@
|
|||
open nat
|
||||
|
||||
example (x y : nat) (H1 : sigma.pr1 ⟨x, y⟩ = 0) : x = 0 :=
|
||||
begin
|
||||
rewrite ▸* at H1,
|
||||
rewrite H1
|
||||
end
|
12
tests/lean/run/rewriter14.lean
Normal file
12
tests/lean/run/rewriter14.lean
Normal file
|
@ -0,0 +1,12 @@
|
|||
import data.nat
|
||||
open nat
|
||||
|
||||
definition f [unfold-c 2] (x y z : nat) : nat :=
|
||||
x + y + z
|
||||
|
||||
attribute of_num [unfold-c 1]
|
||||
|
||||
example (x y : nat) (H1 : f x 0 0 = 0) : x = 0 :=
|
||||
begin
|
||||
rewrite [▸* at H1, 4>add_zero at H1, H1]
|
||||
end
|
Loading…
Reference in a new issue