From d4d538cad85ce5f8f971ae359e3d4d26d37435c2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Apr 2022 12:34:39 -0700
Subject: [PATCH] fix: counterexample generation for new `match` encoding

---
 src/Lean/Meta/Match/Match.lean                        |  2 +-
 .../matchMissingCasesAsStuckError.lean.expected.out   |  2 +-
 tests/lean/matchUnknownFVarBug.lean.expected.out      | 11 ++++++-----
 tests/lean/rwEqThms.lean.expected.out                 |  2 +-
 4 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index edcfecfa5e..40c2c5f0f5 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -838,7 +838,7 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := do
     withAlts motive discrs discrInfos lhss fun alts minors => do
       let mvar ← mkFreshExprMVar mvarType
       trace[Meta.Match.debug] "goal\n{mvar.mvarId!}"
-      let examples := discrs.toList.map fun discr => Example.var discr.fvarId!
+      let examples := discrs'.toList.map fun discr => Example.var discr.fvarId!
       let (_, s) ← (process { mvarId := mvar.mvarId!, vars := discrs'.toList, alts := alts, examples := examples }).run {}
       let val ← mkLambdaFVars discrs' mvar
       trace[Meta.Match.debug] "matcher\nvalue: {val}\ntype: {← inferType val}"
diff --git a/tests/lean/matchMissingCasesAsStuckError.lean.expected.out b/tests/lean/matchMissingCasesAsStuckError.lean.expected.out
index e8e5d28026..08f8c89841 100644
--- a/tests/lean/matchMissingCasesAsStuckError.lean.expected.out
+++ b/tests/lean/matchMissingCasesAsStuckError.lean.expected.out
@@ -1,2 +1,2 @@
 matchMissingCasesAsStuckError.lean:2:2-2:7: error: missing cases:
-none, _
+none
diff --git a/tests/lean/matchUnknownFVarBug.lean.expected.out b/tests/lean/matchUnknownFVarBug.lean.expected.out
index 3c34e589a7..cd7e2626a9 100644
--- a/tests/lean/matchUnknownFVarBug.lean.expected.out
+++ b/tests/lean/matchUnknownFVarBug.lean.expected.out
@@ -1,9 +1,10 @@
 matchUnknownFVarBug.lean:2:2-2:7: error: missing cases:
-(some (Nat.succ _)), Eq.refl, (some _), Eq.refl
-none, Eq.refl, none, Eq.refl
+(some (Nat.succ _)), (some _)
+(some (Nat.succ _)), none
+none, (some _)
+none, none
 matchUnknownFVarBug.lean:3:18-3:19: error: unsolved goals
-n? : Option Nat
+n? x✝ : Option Nat
 h : n? = some 0
-x✝ : Option Nat
-h' : some 0 = x✝
+h' : n? = x✝
 ⊢ False
diff --git a/tests/lean/rwEqThms.lean.expected.out b/tests/lean/rwEqThms.lean.expected.out
index 2a26f39731..4acc39cb37 100644
--- a/tests/lean/rwEqThms.lean.expected.out
+++ b/tests/lean/rwEqThms.lean.expected.out
@@ -2,7 +2,7 @@
 a : α
 as bs : List α
 h : bs = a :: as
-⊢ List.length (?a_1 :: as) = List.length bs
+⊢ List.length (?a :: as) = List.length bs
 
 case a
 α : Type ?u