fix: bug at markNestedProofs in grind

2026-03-19 19:34:13 +00:00 · 2025-01-01 17:55:20 -08:00
2 changed files with 9 additions and 3 deletions
--- 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
--- 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