@[reducible, inline]

abbrev Lean.Compiler.LCNF.ToExpr.LevelMap : Type

Equations

• Lean.Compiler.LCNF.ToExpr.LevelMap = Lean.FVarIdMap Nat

@[reducible, inline]

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

Equations

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

@[inline]

def Lean.Compiler.LCNF.ToExpr.mkLambdaM {pu : Purity} (params : Array (Param pu)) (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)

@[inline]

def 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 {pu : Purity} {α : Type} (params : Array (Param pu)) (k : ToExprM α) : ToExprM α

Equations

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

@[inline]

def Lean.Compiler.LCNF.ToExpr.run {α : Type} (x : ToExprM α) (offset : Nat := 0) (levelMap : 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.FunDecl.toExprM {pu : Purity} (decl : FunDecl pu) : ToExpr.ToExprM Expr

partial def Lean.Compiler.LCNF.Code.toExprM {pu : Purity} (code : Code pu) : ToExpr.ToExprM Expr

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

Equations

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

def Lean.Compiler.LCNF.FunDecl.toExpr {pu : Purity} (decl : FunDecl pu) (xs : Array FVarId := #[]) : Expr

Equations

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