@[inline, reducible]

abbrev Lean.Compiler.LCNF.ToExpr.ToExprM (α : Type) : Type

Equations

• Lean.Compiler.LCNF.ToExpr.ToExprM = ReaderT Nat (StateM Lean.Compiler.LCNF.ToExpr.LevelMap)

@[inline, reducible]

abbrev Lean.Compiler.LCNF.ToExpr.mkLambdaM (params : Array Lean.Compiler.LCNF.Param) (e : Lean.Expr) : Lean.Compiler.LCNF.ToExpr.ToExprM Lean.Expr

Equations

• Lean.Compiler.LCNF.ToExpr.mkLambdaM params e = do let __do_lift ← read let __do_lift_1 ← get pure (Lean.Compiler.LCNF.ToExpr.mkLambdaM.go params __do_lift __do_lift_1 (Array.size params) e)

def Lean.Compiler.LCNF.ToExpr.mkLambdaM.go (params : Array Lean.Compiler.LCNF.Param) (offset : Nat) (m : Lean.Compiler.LCNF.ToExpr.LevelMap) (i : Nat) (e : Lean.Expr) : Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

@[inline, reducible]

abbrev Lean.Compiler.LCNF.ToExpr.abstractM (e : Lean.Expr) : Lean.Compiler.LCNF.ToExpr.ToExprM Lean.Expr

Equations

• Lean.Compiler.LCNF.ToExpr.abstractM e = do let __do_lift ← read let __do_lift_1 ← get pure (Lean.Expr.abstract' __do_lift __do_lift_1 e)

@[inline]

def Lean.Compiler.LCNF.ToExpr.withFVar {α : Type} (fvarId : Lean.FVarId) (k : Lean.Compiler.LCNF.ToExpr.ToExprM α) : Lean.Compiler.LCNF.ToExpr.ToExprM α

Equations

• Lean.Compiler.LCNF.ToExpr.withFVar fvarId k = do let offset ← read modify fun s => Lean.FVarIdMap.insert s fvarId offset withReader (fun x => x + 1) k

@[inline]

def Lean.Compiler.LCNF.ToExpr.withParams {α : Type} (params : Array Lean.Compiler.LCNF.Param) (k : Lean.Compiler.LCNF.ToExpr.ToExprM α) : Lean.Compiler.LCNF.ToExpr.ToExprM α

Equations

• Lean.Compiler.LCNF.ToExpr.withParams params k = Lean.Compiler.LCNF.ToExpr.withParams.go params k 0

@[specialize #[]]

partial def Lean.Compiler.LCNF.ToExpr.withParams.go {α : Type} (params : Array Lean.Compiler.LCNF.Param) (k : Lean.Compiler.LCNF.ToExpr.ToExprM α) (i : Nat) : Lean.Compiler.LCNF.ToExpr.ToExprM α

@[inline]

def Lean.Compiler.LCNF.ToExpr.run {α : Type} (x : Lean.Compiler.LCNF.ToExpr.ToExprM α) (offset : optParam Nat 0) (levelMap : optParam Lean.Compiler.LCNF.ToExpr.LevelMap ∅) : α

Equations

• Lean.Compiler.LCNF.ToExpr.run x offset levelMap = StateT.run' (ReaderT.run x offset) levelMap

@[inline]

def Lean.Compiler.LCNF.ToExpr.run' {α : Type} (x : Lean.Compiler.LCNF.ToExpr.ToExprM α) (xs : Array Lean.FVarId) : α

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Compiler.LCNF.FunDeclCore.toExprM (decl : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.ToExpr.ToExprM Lean.Expr

partial def Lean.Compiler.LCNF.Code.toExprM (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.ToExpr.ToExprM Lean.Expr

def Lean.Compiler.LCNF.Code.toExpr (code : Lean.Compiler.LCNF.Code) (xs : optParam (Array Lean.FVarId) #[]) : Lean.Expr

Equations

• Lean.Compiler.LCNF.Code.toExpr code xs = Lean.Compiler.LCNF.ToExpr.run' (Lean.Compiler.LCNF.Code.toExprM code) xs

def Lean.Compiler.LCNF.FunDeclCore.toExpr (decl : Lean.Compiler.LCNF.FunDecl) (xs : optParam (Array Lean.FVarId) #[]) : Lean.Expr

Equations

• Lean.Compiler.LCNF.FunDeclCore.toExpr decl xs = Lean.Compiler.LCNF.ToExpr.run' (Lean.Compiler.LCNF.FunDeclCore.toExprM decl) xs

def Lean.Compiler.LCNF.Decl.toExpr (decl : Lean.Compiler.LCNF.Decl) : Lean.Expr

Equations

• One or more equations did not get rendered due to their size.