max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: typo (#4635)

Browse source
This commit is contained in:
Alok Singh 2024-07-02 22:14:09 -07:00 • committed by GitHub
parent f5fd962a25
commit 2cd2364974
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/BuiltinNotation.lean
View file

@ -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])))` -/