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

• typeParams : FVarIdHashSet

@[reducible, inline]

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

Equations

• Lean.Compiler.LCNF.ToMonoM = StateRefT' IO.RealWorld Lean.Compiler.LCNF.ToMonoM.State Lean.Compiler.LCNF.CompilerM

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

Equations

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

@[inline]

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.argToMono Lean.Compiler.LCNF.Arg.erased = pure Lean.Compiler.LCNF.Arg.erased
• Lean.Compiler.LCNF.argToMono (Lean.Compiler.LCNF.Arg.type expr h) = pure Lean.Compiler.LCNF.Arg.erased

def Lean.Compiler.LCNF.argsToMonoWithFnType (args : Array (Arg Purity.pure)) (type : Expr) : ToMonoM (Array (Arg Purity.pure))

Equations

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

def Lean.Compiler.LCNF.argsToMonoRedArg (args : Array (Arg Purity.pure)) (params : Array (Param Purity.pure)) (redArgs : Array (Arg Purity.pure)) : ToMonoM (Array (Arg Purity.pure))

Equations

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

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

Equations

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

partial def Lean.Compiler.LCNF.LetValue.toMono (e : LetValue Purity.pure) : ToMonoM (LetValue Purity.pure)

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

Equations

• decl.toMono = do let type ← liftM (Lean.Compiler.LCNF.toMonoType decl.type) let value ← decl.value.toMono liftM (decl.update type value)

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

Equations

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

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

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

Convert cases Decidable => Bool

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

Eliminate cases for Nat.

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

Eliminate cases for Int.

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

Eliminate cases for UInt types.

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

Eliminate cases for `Array.

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

Eliminate cases for `ByteArray.

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

Eliminate cases for `FloatArray.

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

Eliminate cases for `String.

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

Eliminate cases for `Thunk.

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

Eliminate cases for `Task.

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

Eliminate cases for trivial structure. See hasTrivialStructure?

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

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

Equations

• decl.toMono = StateRefT'.run' (Lean.Compiler.LCNF.Decl.toMono.go✝ decl) { }

def Lean.Compiler.LCNF.toMono : Pass

Equations

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