fix: bug at markNestedProofs in grind

leanprover · Jan 2, 2025 · e802056 · e802056
1 parent a8d09da
commit e802056
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 3 deletions.
diff --git a/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean b/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean
@@ -28,9 +28,9 @@ where
       | .bvar .. => unreachable!
       -- See comments on `Canon.lean` for why we do not visit these cases.
       | .letE .. | .forallE .. | .lam ..
-      | .const .. | .lit .. | .mvar .. | .sort .. | .fvar ..
-      | .proj ..
-      | .mdata ..  => return e
+      | .const .. | .lit .. | .mvar .. | .sort .. | .fvar .. => return e
+      | .proj _ _ b => return e.updateProj! (← visit b)
+      | .mdata _ b  => return e.updateMData! (← visit b)
       -- We only visit applications
       | .app .. =>
         -- Check whether it is cached

diff --git a/tests/lean/run/grind_nested_proof_issue.lean b/tests/lean/run/grind_nested_proof_issue.lean
@@ -0,0 +1,6 @@
+example (as bs : Array α) (v : α)
+        (i : Nat)
+        (h₁ : i < as.size)
+        (h₂ : bs = as.set i v)
+        : (as.set i v).size = as.size → as.size = bs.size := by
+  grind