fix: auto/option params should not break sorry (#4132)

closes #2649
leanprover · May 11, 2024 · 7db8e64 · 7db8e64
1 parent 147aeae
commit 7db8e64
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
@@ -205,7 +205,7 @@ private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do
   | _                                        => Macro.throwUnsupported
 
 @[builtin_term_elab «sorry»] def elabSorry : TermElab := fun stx expectedType? => do
-  let stxNew ← `(sorryAx _ false)
+  let stxNew ← `(@sorryAx _ false) -- Remark: we use `@` to ensure `sorryAx` will not consume auot params
   withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
 
 /-- Return syntax `Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))` -/

diff --git a/tests/lean/run/2649.lean b/tests/lean/run/2649.lean
@@ -0,0 +1,3 @@
+def foo1 : (_ : Nat := 0) → Nat := sorry
+
+def foo2 : (_ : Nat := by exact 0) → Nat := sorry