DestructProducts: fix incorrect mvar handling

leanprover-community · Oct 2, 2023 · 0194095 · 0194095
1 parent 4f8b397
commit 0194095
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/Aesop/BuiltinRules/DestructProducts.lean b/Aesop/BuiltinRules/DestructProducts.lean
@@ -50,7 +50,7 @@ private def destructProductHyp (goal : MVarId) (hyp : FVarId)
       goal.withContext $ check prf
       let [goal] ← goal.apply prf
         | throwError "destructProducts: apply did not return exactly one goal"
-      discard $ goal.introN (genHyps.size - 1)
+      let (_, goal) ← goal.introN (genHyps.size - 1)
       let (_, goal) ← goal.introN 2
       goal.clear hyp
 

diff --git a/AesopTest/DestructProducts.lean b/AesopTest/DestructProducts.lean
@@ -43,3 +43,7 @@ example {p : α → Type} (h : Σ a, p a) : Sig α p := by
 
 example {p : α → Type} (h : Σ' a, p a) : Sig α p := by
   aesop
+
+-- Test case for a bug reported by Jakob von Raumer.
+example (x y : α × α) (h: p ∧ (x = y)) : x = y := by
+  aesop (simp_options := { enabled := false })