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

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

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-27 16:17:31 +01:00
parent fbec9053dc
commit 9d8d62a983
1 changed files with 18 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
tests/lean/run/do_match_else.lean
View file

@ -5,11 +5,25 @@ set_option pp.all true
example (a b c x y : nat) (H : nat.add (nat.add x y) y = 0) : true :=
by do
a ← get_local "a", b ← get_local "b", c ← get_local "c",
H ← get_local "H" >>= infer_type,
(lhs, rhs) ← match_eq H,
nat_add : expr ← mk_const ("nat" <.> "add"),
p : pattern ← mk_pattern [] [a, b] (nat_add a b) [nat_add b a, a, b],
trace (pattern.output p),
H ← get_local "H" >>= infer_type,
lhs_rhs ← match_eq H,
[v₁, v₂, v₃] ← match_pattern p (prod.pr1 lhs_rhs) | failed,
trace v₁,
[v₁, v₂, v₃] ← match_pattern p lhs | failed,
trace v₁, trace v₂, trace v₃,
constructor
print "------------------"
example (f : nat → nat) (a b c x y : nat) (H : nat.add (nat.add (f (f x)) y) y = 0) : true :=
by do
a ← get_local "a", b ← get_local "b", c ← get_local "c",
H ← get_local "H" >>= infer_type,
(lhs, rhs) ← match_eq H,
nat_add : expr ← mk_const ("nat" <.> "add"),
p : pattern ← mk_pattern [] [a, b] (nat_add (nat_add a b) b) [nat_add (nat_add b b) (nat_add a a b), a, b],
trace (pattern.output p),
[v₁, v₂, v₃] ← match_pattern p lhs | failed,
trace v₁, trace v₂, trace v₃,
constructor