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

chore(tests/lean/run): fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2017-12-06 16:04:24 -08:00
parent c5ed881c59
commit 9fff5ff710
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -13,6 +13,6 @@ by do
nat_add : expr ← mk_const `nat.add,
p : pattern ← mk_pattern [] [a, b] (app2 nat_add a b) [] [app2 nat_add b a, a, b],
trace (pattern.moutput p),
[v₁, v₂, v₃] ← match_pattern p lhs | failed,
(_, [v₁, v₂, v₃]) ← match_pattern p lhs | failed,
trace v₁, trace v₂, trace v₃,
constructor

2
tests/lean/run/match_pattern2.lean
View file

@ -31,7 +31,7 @@ by do
H ← get_local `H >>= infer_type,
(lhs, rhs) ← match_eq H,
p ← mk_pattern_for_constant $ `add.comm,
[rhs_inst, prf] ← match_pattern p lhs | failed,
(_, [rhs_inst, prf]) ← match_pattern p lhs | failed,
trace "match rhs",
trace rhs_inst,
trace "proof lhs = rhs",