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

• typeParams : FVarIdSet

@[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) : ToMonoM Param

Equations

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

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

Equations

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

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

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) = pure Lean.Compiler.LCNF.Arg.erased

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.toMono : Pass

Equations

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