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

fix: missing mkRecAppWithSyntax

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-14 09:29:54 -07:00
parent 02145f66cf
commit 9988faf8bd
1 changed files with 11 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Lean/Elab/App.lean
View file

@ -962,19 +962,21 @@ private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array A
else
withRef f <| mergeFailures candidates
private def annotateIfRec (stx : Syntax) (e : Expr) : TermElabM Expr := do
let resultFn := e.getAppFn
if resultFn.isFVar then
let localDecl ← getLocalDecl resultFn.fvarId!
if localDecl.isAuxDecl then
return mkRecAppWithSyntax e stx
return e
@[builtinTermElab app] def elabApp : TermElab := fun stx expectedType? =>
withoutPostponingUniverseConstraints do
let (f, namedArgs, args, ellipsis) ← expandApp stx
let result ← elabAppAux f namedArgs args (ellipsis := ellipsis) expectedType?
let resultFn := result.getAppFn
if resultFn.isFVar then
let localDecl ← getLocalDecl resultFn.fvarId!
if localDecl.isAuxDecl then
return mkRecAppWithSyntax result stx
return result
annotateIfRec stx (← elabAppAux f namedArgs args (ellipsis := ellipsis) expectedType?)
private def elabAtom : TermElab := fun stx expectedType? =>
elabAppAux stx #[] #[] (ellipsis := false) expectedType?
private def elabAtom : TermElab := fun stx expectedType? => do
annotateIfRec stx (← elabAppAux stx #[] #[] (ellipsis := false) expectedType?)
@[builtinTermElab ident] def elabIdent : TermElab := elabAtom
/-- `x@e` matches the pattern `e` and binds its value to the identifier `x`. -/