@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Lean.Compiler.LCNF.ToExpr.mkLambdaM (params : Array Param) (e : Expr) : ToExprM 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 params.size e)

@[irreducible]

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

Equations

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

@[reducible, inline]

abbrev Lean.Compiler.LCNF.ToExpr.abstractM (e : Expr) : ToExprM 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 : FVarId) (k : ToExprM α) : ToExprM α

Equations

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

@[inline]

def Lean.Compiler.LCNF.ToExpr.withParams {α : Type} (params : Array Param) (k : ToExprM α) : 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 Param) (k : ToExprM α) (i : Nat) : ToExprM α

@[inline]

def Lean.Compiler.LCNF.ToExpr.run {α : Type} (x : ToExprM α) (offset : Nat := 0) (levelMap : 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 : ToExprM α) (xs : Array FVarId) : α

Equations

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

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

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

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

Equations

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

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

Equations

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