From 2cd23649749dc55d9216092ef86315843b463ad1 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Tue, 2 Jul 2024 22:14:09 -0700 Subject: [PATCH] chore: typo (#4635) --- src/Lean/Elab/BuiltinNotation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 65b12af639..1f41718124 100644 --- 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) -- Remark: we use `@` to ensure `sorryAx` will not consume auot params + let stxNew ← `(@sorryAx _ false) -- Remark: we use `@` to ensure `sorryAx` will not consume auto 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])))` -/