structure Lean.Compiler.LCNF.ToMonoM.State : Type

• typeParams : FVarIdHashSet
• noncomputableVars : Std.HashMap FVarId Name

@[reducible, inline]

abbrev Lean.Compiler.LCNF.ToMonoM (α : Type) : Type

def Lean.Compiler.LCNF.Param.toMono (param : Param) : ToMonoM Param

def Lean.Compiler.LCNF.isTrivialConstructorApp? (declName : Name) (args : Array Arg) : ToMonoM (Option LetValue)

def Lean.Compiler.LCNF.checkFVarUse (fvarId : FVarId) : ToMonoM Unit

def Lean.Compiler.LCNF.checkFVarUseDeferred (resultFVar fvarId : FVarId) : ToMonoM Unit

@[inline]

def Lean.Compiler.LCNF.argToMonoBase (check : FVarId → ToMonoM Unit) (arg : Arg) : ToMonoM Arg

def Lean.Compiler.LCNF.argToMono (arg : Arg) : ToMonoM Arg

def Lean.Compiler.LCNF.argToMonoDeferredCheck (resultFVar : FVarId) (arg : Arg) : ToMonoM Arg

def Lean.Compiler.LCNF.ctorAppToMono (resultFVar : FVarId) (ctorInfo : ConstructorVal) (args : Array Arg) : ToMonoM LetValue

partial def Lean.Compiler.LCNF.LetValue.toMono (e : LetValue) (resultFVar : FVarId) : ToMonoM LetValue

def Lean.Compiler.LCNF.LetDecl.toMono (decl : LetDecl) : ToMonoM LetDecl

def Lean.Compiler.LCNF.mkFieldParamsForComputedFields (ctorType : Expr) (numParams numNewFields : Nat) (oldFields : Array Param) : ToMonoM (Array Param)

partial def Lean.Compiler.LCNF.FunDecl.toMono (decl : FunDecl) : ToMonoM FunDecl

partial def Lean.Compiler.LCNF.decToMono (c : Cases) : (c.typeName == `Decidable) = true → ToMonoM Code

Convert cases Decidable => Bool

partial def Lean.Compiler.LCNF.casesNatToMono (c : Cases) : (c.typeName == `Nat) = true → ToMonoM Code

Eliminate cases for Nat.

partial def Lean.Compiler.LCNF.casesIntToMono (c : Cases) : (c.typeName == `Int) = true → ToMonoM Code

Eliminate cases for Int.

partial def Lean.Compiler.LCNF.casesUIntToMono (c : Cases) (uintName : Name) : (c.typeName == uintName) = true → ToMonoM Code

Eliminate cases for UInt types.

partial def Lean.Compiler.LCNF.casesArrayToMono (c : Cases) : (c.typeName == `Array) = true → ToMonoM Code

Eliminate cases for `Array.

partial def Lean.Compiler.LCNF.casesByteArrayToMono (c : Cases) : (c.typeName == `ByteArray) = true → ToMonoM Code

Eliminate cases for `ByteArray.

partial def Lean.Compiler.LCNF.casesFloatArrayToMono (c : Cases) : (c.typeName == `FloatArray) = true → ToMonoM Code

Eliminate cases for `FloatArray.

partial def Lean.Compiler.LCNF.casesStringToMono (c : Cases) : (c.typeName == `String) = true → ToMonoM Code

Eliminate cases for `String.

partial def Lean.Compiler.LCNF.casesThunkToMono (c : Cases) : (c.typeName == `Thunk) = true → ToMonoM Code

Eliminate cases for `Thunk.

partial def Lean.Compiler.LCNF.casesTaskToMono (c : Cases) : (c.typeName == `Task) = true → ToMonoM Code

Eliminate cases for `Task.

partial def Lean.Compiler.LCNF.trivialStructToMono (info : TrivialStructureInfo) (c : Cases) : ToMonoM Code

Eliminate cases for trivial structure. See hasTrivialStructure?

partial def Lean.Compiler.LCNF.Code.toMono (code : Code) : ToMonoM Code

def Lean.Compiler.LCNF.Decl.toMono (decl : Decl) : CompilerM Decl

def Lean.Compiler.LCNF.Decl.toMono.go (decl : Decl) : ToMonoM Decl

def Lean.Compiler.LCNF.toMono : Pass