- id : Lean.Syntax
- type : Lean.Syntax
- bi : Lean.BinderInfo
Equations
- Lean.Elab.Term.declareTacticSyntax tactic = Lean.withFreshMacroScope do let name ← Lean.MonadQuotation.addMacroScope `_auto let type : Lean.Expr := Lean.mkConst `Lean.Syntax let tactic ← Lean.Elab.Term.quoteAutoTactic tactic let val ← Lean.Elab.Term.elabTerm tactic (some type) true true let val ← liftM (Lean.Meta.instantiateMVars val) let cls : Lean.Name := `Elab.autoParam let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.TermElabM Lean.Name := fun y => let decl := Lean.Declaration.defnDecl { toConstantVal := { name := name, levelParams := [], type := type }, value := val, hints := Lean.ReducibilityHints.opaque, safety := Lean.DefinitionSafety.safe }; do Lean.addDecl decl Lean.compileDecl decl pure name if a = true then do let y ← Lean.addTrace cls (Lean.MessageData.ofExpr val) _do_jp y else do let y ← pure PUnit.unit _do_jp y
def
Lean.Elab.Term.elabBindersEx
{α : Type}
(binders : Array Lean.Syntax)
(k : Array (Lean.Syntax × Lean.Expr) → Lean.Elab.TermElabM α)
:
Equations
- Lean.Elab.Term.elabBindersEx binders k = Lean.Elab.Term.withoutPostponingUniverseConstraints (if Array.isEmpty binders = true then k #[] else Lean.Elab.Term.elabBindersAux binders k)
Equations
- Lean.Elab.Term.elabForall stx x = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.forall = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; let term := discr; let binders := Lean.Syntax.getArgs discr_2; Lean.Elab.Term.elabBinders binders fun xs => do let e ← Lean.Elab.Term.elabType term liftM (Lean.Meta.mkForallFVars xs e false true) else let discr := stx; Lean.Elab.throwUnsupportedSyntax
def
Lean.Elab.Term.elabBinders
{α : Type}
(binders : Array Lean.Syntax)
(k : Array Lean.Expr → Lean.Elab.TermElabM α)
:
Equations
- Lean.Elab.Term.elabBinders binders k = Lean.Elab.Term.elabBindersEx binders fun fvars => k (Array.map (fun a => a.snd) fvars)
def
Lean.Elab.Term.elabBinder
{α : Type}
(binder : Lean.Syntax)
(x : Lean.Expr → Lean.Elab.TermElabM α)
:
Equations
- Lean.Elab.Term.elabBinder binder x = Lean.Elab.Term.elabBinders #[binder] fun fvars => x (Array.getOp fvars 0)
Equations
- Lean.Elab.Term.elabArrow stx x = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.arrow = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr 2; let rng := discr; let dom := discr_1; do let dom ← Lean.Elab.Term.elabType dom let rng ← Lean.Elab.Term.elabType rng let a ← Lean.MonadQuotation.addMacroScope `a pure (Lean.mkForall a Lean.BinderInfo.default dom rng) else let discr := stx; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Term.elabDepArrow stx x = let binder := Lean.Syntax.getOp stx 0; let term := Lean.Syntax.getOp stx 2; Lean.Elab.Term.elabBinders #[binder] fun xs => do let a ← Lean.Elab.Term.elabType term liftM (Lean.Meta.mkForallFVars xs a false true)
Equations
- Lean.Elab.Term.expandFunBinders binders body = (fun loop => loop body 0 #[]) (Lean.Elab.Term.expandFunBinders.loop binders)
partial def
Lean.Elab.Term.expandFunBinders.loop
(binders : Array Lean.Syntax)
(body : Lean.Syntax)
(i : Nat)
(newBinders : Array Lean.Syntax)
:
- fvars : Array Lean.Expr
- lctx : Lean.LocalContext
- localInsts : Lean.LocalInstances
- expectedType? : Option Lean.Expr
partial def
Lean.Elab.Term.FunBinders.elabFunBindersAux
(binders : Array Lean.Syntax)
(i : Nat)
(s : Lean.Elab.Term.FunBinders.State)
:
def
Lean.Elab.Term.elabFunBinders
{α : Type}
(binders : Array Lean.Syntax)
(expectedType? : Option Lean.Expr)
(x : Array Lean.Expr → Option Lean.Expr → Lean.Elab.TermElabM α)
:
Equations
- Lean.Elab.Term.elabFunBinders binders expectedType? x = if Array.isEmpty binders = true then x #[] expectedType? else do let lctx ← Lean.getLCtx let localInsts ← liftM Lean.Meta.getLocalInstances let s ← Lean.Elab.Term.FunBinders.elabFunBindersAux binders 0 { fvars := #[], lctx := lctx, localInsts := localInsts, expectedType? := expectedType? } Lean.Meta.resettingSynthInstanceCacheWhen (decide (Array.size s.localInsts > Array.size localInsts)) (Lean.Meta.withLCtx s.lctx s.localInsts (x s.fvars s.expectedType?))
Equations
- Lean.Elab.Term.expandWhereDecls whereDecls body = let discr := whereDecls; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.whereDecls = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; match OptionM.run (Array.sequenceMap (Lean.Syntax.getArgs discr_2) fun x => let discr := x; if Lean.Syntax.isOfKind discr `group = true then let discr_3 := Lean.Syntax.getArg discr 0; cond (Lean.Syntax.isOfKind discr_3 `Lean.Parser.Term.letRecDecl) (let discr_4 := Lean.Syntax.getArg discr 1; let yes := fun x => let decls := discr_3; some decls; if Lean.Syntax.isNone discr_4 = true then yes () else let discr_5 := discr_4; if Lean.Syntax.matchesNull discr_5 1 = true then let discr := Lean.Syntax.getArg discr_5 0; yes () else let discr_6 := discr_4; let discr := Lean.Syntax.getArg discr 1; none) (let discr_4 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; none) else let discr := x; none) with | some decls => do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letrec #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.atom info "let", Lean.Syntax.atom info "rec"], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letRecDecls #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.Syntax.SepArray.ofElems decls).elemsAndSeps)], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], body]) | none => let discr := Lean.Syntax.getArg discr 1; Lean.Macro.throwUnsupported else let discr := whereDecls; Lean.Macro.throwUnsupported
Equations
- Lean.Elab.Term.expandWhereDeclsOpt whereDeclsOpt body = if Lean.Syntax.isNone whereDeclsOpt = true then pure body else Lean.Elab.Term.expandWhereDecls (Lean.Syntax.getOp whereDeclsOpt 0) body
def
Lean.Elab.Term.expandMatchAltsIntoMatch
(ref : Lean.Syntax)
(matchAlts : Lean.Syntax)
(tactic : optParam Bool false)
:
Equations
- Lean.Elab.Term.expandMatchAltsIntoMatch ref matchAlts tactic = Lean.withRef ref (Lean.Elab.Term.expandMatchAltsIntoMatchAux matchAlts tactic (Lean.Elab.Term.getMatchAltsNumPatterns matchAlts) #[])
Equations
- Lean.Elab.Term.expandMatchAltsIntoMatchTactic ref matchAlts = Lean.withRef ref (Lean.Elab.Term.expandMatchAltsIntoMatchAux matchAlts true (Lean.Elab.Term.getMatchAltsNumPatterns matchAlts) #[])
Equations
- Lean.Elab.Term.expandMatchAltsWhereDecls matchAltsWhereDecls = let matchAlts := Lean.Syntax.getOp matchAltsWhereDecls 0; let whereDeclsOpt := Lean.Syntax.getOp matchAltsWhereDecls 1; (fun loop => loop (Lean.Elab.Term.getMatchAltsNumPatterns matchAlts) #[]) (Lean.Elab.Term.expandMatchAltsWhereDecls.loop matchAlts whereDeclsOpt)
def
Lean.Elab.Term.expandMatchAltsWhereDecls.loop
(matchAlts : Lean.Syntax)
(whereDeclsOpt : Lean.Syntax)
(i : Nat)
(discrs : Array Lean.Syntax)
:
Equations
- Lean.Elab.Term.expandMatchAltsWhereDecls.loop matchAlts whereDeclsOpt 0 discrs = do let matchStx ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.match #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.mkSepArray (Array.map (fun discrs => Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr #[Lean.Syntax.node Lean.SourceInfo.none `null #[], discrs]) discrs) (Lean.mkAtom ","))), Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "with", matchAlts]) if Lean.Syntax.isNone whereDeclsOpt = true then pure matchStx else Lean.Elab.Term.expandWhereDeclsOpt whereDeclsOpt matchStx
- Lean.Elab.Term.expandMatchAltsWhereDecls.loop matchAlts whereDeclsOpt (Nat.succ n) discrs = Lean.withFreshMacroScope do let d ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicit #[Lean.Syntax.atom info "@", Lean.Syntax.ident info (String.toSubstring "x") (Lean.addMacroScope mainModule `x scp) []]) let body ← Lean.Elab.Term.expandMatchAltsWhereDecls.loop matchAlts whereDeclsOpt n (Array.push discrs d) let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicit #[Lean.Syntax.atom info "@", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "x") (Lean.addMacroScope mainModule `x scp) []], Lean.Syntax.atom info "=>", body]]])
Equations
- Lean.Elab.Term.expandFun x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.fun = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.basicFun = true then let discr := Lean.Syntax.getArg discr_2 0; let discr_3 := Lean.Syntax.getArg discr_2 1; let discr_4 := Lean.Syntax.getArg discr_2 2; let body := discr_4; let binders := Lean.Syntax.getArgs discr; do let discr ← Lean.Elab.Term.expandFunBinders binders body let x : Array Lean.Syntax × Lean.Syntax × Bool := discr match x with | (binders, body, expandedPattern) => if expandedPattern = true then do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] binders), Lean.Syntax.atom info "=>", body]]) else Lean.Macro.throwUnsupported else let discr_3 := Lean.Syntax.getArg discr 1; cond (Lean.Syntax.isOfKind discr_3 `Lean.Parser.Term.matchAlts) (let m := discr_3; let stx := discr; Lean.Elab.Term.expandMatchAltsIntoMatch stx m false) (let discr := Lean.Syntax.getArg discr 1; Lean.Macro.throwUnsupported) else let discr := x; Lean.Macro.throwUnsupported
Equations
- Lean.Elab.Term.precheckFun x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.fun = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.basicFun = true then let discr := Lean.Syntax.getArg discr_2 0; let discr_3 := Lean.Syntax.getArg discr_2 1; let discr_4 := Lean.Syntax.getArg discr_2 2; let body := discr_4; let binders := Lean.Syntax.getArgs discr; do let discr ← Lean.Elab.liftMacroM (Lean.Elab.Term.expandFunBinders binders body) let x : Array Lean.Syntax × Lean.Syntax × Bool := discr match x with | (binders, body, expandedPattern) => let ids := #[]; do let r ← forIn binders ids fun b r => let ids := r; do let a ← liftM (Lean.Elab.Term.matchBinder b) let r ← forIn a ids fun v r => let ids := r; do Lean.Elab.Term.Quotation.withNewLocals ids (Lean.Elab.Term.Quotation.precheck v.type) let ids : Array Lean.Name := Array.push ids (Lean.Syntax.getId v.id) pure PUnit.unit pure (ForInStep.yield ids) let x : Array Lean.Name := r let ids : Array Lean.Name := x pure PUnit.unit pure (ForInStep.yield ids) let x : Array Lean.Name := r let ids : Array Lean.Name := x Lean.Elab.Term.Quotation.withNewLocals ids (Lean.Elab.Term.Quotation.precheck body) else let discr := Lean.Syntax.getArg discr 1; Lean.Elab.throwUnsupportedSyntax else let discr := x; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Term.elabFun stx expectedType? = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.fun = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.basicFun = true then let discr := Lean.Syntax.getArg discr_2 0; let discr_3 := Lean.Syntax.getArg discr_2 1; let discr_4 := Lean.Syntax.getArg discr_2 2; let body := discr_4; let binders := Lean.Syntax.getArgs discr; do let discr ← Lean.Elab.liftMacroM (Lean.Elab.Term.expandFunBinders binders body) let x : Array Lean.Syntax × Lean.Syntax × Bool := discr match x with | (binders, body, expandedPattern) => Lean.Elab.Term.elabFunBinders binders expectedType? fun xs expectedType? => do let e ← Lean.Elab.Term.elabTermEnsuringType body expectedType? true true none liftM (Lean.Meta.mkLambdaFVars xs e false true) else let discr := Lean.Syntax.getArg discr 1; Lean.Elab.throwUnsupportedSyntax else let discr := stx; Lean.Elab.throwUnsupportedSyntax
def
Lean.Elab.Term.elabLetDeclAux
(id : Lean.Syntax)
(binders : Array Lean.Syntax)
(typeStx : Lean.Syntax)
(valStx : Lean.Syntax)
(body : Lean.Syntax)
(expectedType? : Option Lean.Expr)
(useLetExpr : Bool)
(elabBodyFirst : Bool)
(usedLetOnly : Bool)
:
Equations
- Lean.Elab.Term.elabLetDeclAux id binders typeStx valStx body expectedType? useLetExpr elabBodyFirst usedLetOnly = do let discr ← Lean.Elab.Term.elabBinders binders fun xs => do let type ← Lean.Elab.Term.elabType typeStx Lean.Elab.Term.registerCustomErrorIfMVar type typeStx (Function.comp Lean.MessageData.ofFormat Lean.format "failed to infer 'let' declaration type") if elabBodyFirst = true then do let type ← liftM (Lean.Meta.mkForallFVars xs type false true) let val ← liftM (Lean.Meta.mkFreshExprMVar (some type) Lean.MetavarKind.natural Lean.Name.anonymous) pure (type, val, Array.size xs) else do let val ← Lean.Elab.Term.elabTermEnsuringType valStx (some type) true true none let type ← liftM (Lean.Meta.mkForallFVars xs type false true) let val ← liftM (Lean.Meta.mkLambdaFVars xs val false false) pure (type, val, Array.size xs) let x : Lean.Expr × Lean.Expr × Nat := discr match x with | (type, val, arity) => let cls := `Elab.let.decl; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.TermElabM Lean.Expr := fun y => let _do_jp := fun result => let _do_jp := fun y => pure result; if elabBodyFirst = true then do let y ← Lean.Meta.forallBoundedTelescope type (some arity) fun xs type => do let valResult ← Lean.Elab.Term.elabTermEnsuringType valStx (some type) true true none let valResult ← liftM (Lean.Meta.mkLambdaFVars xs valResult false false) let a ← liftM (Lean.Meta.isDefEq val valResult) if a = true then pure PUnit.unit else Lean.throwError (Lean.toMessageData "unexpected error when elaborating 'let'") _do_jp y else do let y ← pure PUnit.unit _do_jp y; if useLetExpr = true then do let y ← Lean.Meta.withLetDecl (Lean.Syntax.getId id) type val fun x => do Lean.Elab.Term.addLocalVarInfo id x let body ← Lean.Elab.Term.elabTermEnsuringType body expectedType? true true none let body ← liftM (Lean.Meta.instantiateMVars body) liftM (Lean.Meta.mkLetFVars #[x] body usedLetOnly) _do_jp y else do let f ← Lean.Meta.withLocalDecl (Lean.Syntax.getId id) Lean.BinderInfo.default type fun x => do Lean.Elab.Term.addLocalVarInfo id x let body ← Lean.Elab.Term.elabTermEnsuringType body expectedType? true true none let body ← liftM (Lean.Meta.instantiateMVars body) liftM (Lean.Meta.mkLambdaFVars #[x] body false false) let y ← pure (Lean.mkLetFunAnnotation (Lean.mkApp f val)) _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData (Lean.Syntax.getId id) ++ Lean.toMessageData " : " ++ Lean.toMessageData type ++ Lean.toMessageData " := " ++ Lean.toMessageData val ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y
- id : Lean.Syntax
- binders : Array Lean.Syntax
- type : Lean.Syntax
- value : Lean.Syntax
Equations
- Lean.Elab.Term.mkLetIdDeclView letIdDecl = let id := Lean.Syntax.getOp letIdDecl 0; let binders := Lean.Syntax.getArgs (Lean.Syntax.getOp letIdDecl 1); let optType := Lean.Syntax.getOp letIdDecl 2; let type := Lean.Elab.Term.expandOptType id optType; let value := Lean.Syntax.getOp letIdDecl 4; { id := id, binders := binders, type := type, value := value }
Equations
- Lean.Elab.Term.expandLetEqnsDecl letDecl = let ref := letDecl; let matchAlts := Lean.Syntax.getOp letDecl 3; do let val ← Lean.Elab.Term.expandMatchAltsIntoMatch ref matchAlts false pure (Lean.mkNode `Lean.Parser.Term.letIdDecl #[Lean.Syntax.getOp letDecl 0, Lean.Syntax.getOp letDecl 1, Lean.Syntax.getOp letDecl 2, Lean.mkAtomFrom ref " := ", val])
def
Lean.Elab.Term.elabLetDeclCore
(stx : Lean.Syntax)
(expectedType? : Option Lean.Expr)
(useLetExpr : Bool)
(elabBodyFirst : Bool)
(usedLetOnly : Bool)
:
Equations
- Lean.Elab.Term.elabLetDeclCore stx expectedType? useLetExpr elabBodyFirst usedLetOnly = let ref := stx; let letDecl := Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0; let body := Lean.Syntax.getOp stx 3; if (Lean.Syntax.getKind letDecl == `Lean.Parser.Term.letIdDecl) = true then let x := Lean.Elab.Term.mkLetIdDeclView letDecl; match x with | { id := id, binders := binders, type := type, value := val } => Lean.Elab.Term.elabLetDeclAux id binders type val body expectedType? useLetExpr elabBodyFirst usedLetOnly else if (Lean.Syntax.getKind letDecl == `Lean.Parser.Term.letPatDecl) = true then let pat := Lean.Syntax.getOp letDecl 0; let optType := Lean.Syntax.getOp letDecl 2; let type := Lean.Elab.Term.expandOptType pat optType; let val := Lean.Syntax.getOp letDecl 4; do let stxNew ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letIdDecl #[Lean.Syntax.ident info (String.toSubstring "x") (Lean.addMacroScope mainModule `x scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", type]], Lean.Syntax.atom info ":=", val]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.match #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.ident info (String.toSubstring "x") (Lean.addMacroScope mainModule `x scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "with", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[pat], Lean.Syntax.atom info "=>", body]]]]]) let stxNew : Lean.Syntax := match useLetExpr, elabBodyFirst with | true, false => stxNew | true, true => Lean.Syntax.setKind stxNew `Lean.Parser.Term.let_delayed | false, false => Lean.Syntax.setKind stxNew `Lean.Parser.Term.let_fun | false, true => panicWithPosWithDecl "Lean.Elab.Binders" "Lean.Elab.Term.elabLetDeclCore" 628 24 "unreachable code has been reached" Lean.Elab.Term.withMacroExpansion stx stxNew (Lean.Elab.Term.elabTerm stxNew expectedType? true true) else if (Lean.Syntax.getKind letDecl == `Lean.Parser.Term.letEqnsDecl) = true then do let letDeclIdNew ← Lean.Elab.liftMacroM (Lean.Elab.Term.expandLetEqnsDecl letDecl) let declNew : Lean.Syntax := Lean.Syntax.setArg (Lean.Syntax.getOp stx 1) 0 letDeclIdNew let stxNew : Lean.Syntax := Lean.Syntax.setArg stx 1 declNew Lean.Elab.Term.withMacroExpansion stx stxNew (Lean.Elab.Term.elabTerm stxNew expectedType? true true) else Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Term.elabLetDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? true false false
Equations
- Lean.Elab.Term.elabLetFunDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? false false false
Equations
- Lean.Elab.Term.elabLetDelayedDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? true true false
Equations
- Lean.Elab.Term.elabLetTmpDecl stx expectedType? = Lean.Elab.Term.elabLetDeclCore stx expectedType? true false true