From 9fff5ff7103c12bddcf0271f57fa6df4d8fdbcf8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Dec 2017 16:04:24 -0800 Subject: [PATCH] chore(tests/lean/run): fix tests --- tests/lean/run/do_match_else.lean | 2 +- tests/lean/run/match_pattern2.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/run/do_match_else.lean b/tests/lean/run/do_match_else.lean index bf16e9dfd4..be8e843a34 100644 --- a/tests/lean/run/do_match_else.lean +++ b/tests/lean/run/do_match_else.lean @@ -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 diff --git a/tests/lean/run/match_pattern2.lean b/tests/lean/run/match_pattern2.lean index a5a53bed3b..f0e3c6cee3 100644 --- a/tests/lean/run/match_pattern2.lean +++ b/tests/lean/run/match_pattern2.lean @@ -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",