@[reducible, inline]

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

@[reducible, inline]

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

@[irreducible]

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

@[reducible, inline]

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

@[inline]

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

@[inline]

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

@[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✝ := ∅) : α

@[inline]

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

partial def Lean.Compiler.LCNF.FunDecl.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

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