Lean.Elab.LetRec

Type

Type

Equations

Lean.Elab.Term.elabLetRec stx expectedType? = do let view ← Lean.Elab.Term.mkLetRecDeclView stx Lean.Elab.Term.withAuxLocalDecls view.decls fun fvars => let s := toStream fvars; do let r ← let col := view.decls; forIn col s fun decl r => let s := r; match Stream.next? s with | none => pure (ForInStep.done s) | some (fvar, s') => let s := s'; do Lean.Elab.Term.addTermInfo (Lean.Syntax.getOp decl.ref 0) fvar none none Lean.Name.anonymous true pure (ForInStep.yield s) let x : Subarray Lean.Expr := r let s : Subarray Lean.Expr := x let values ← Lean.Elab.Term.elabLetRecDeclValues view let body ← Lean.Elab.Term.elabTermEnsuringType view.body expectedType? true true none Lean.Elab.Term.registerLetRecsToLift view.decls fvars values let mvars : Array Lean.Expr := Array.map (fun a => a.mvar) view.decls let a ← liftM (Lean.Meta.mkLambdaFVars fvars body false true) pure (Lean.mkAppN a mvars)