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

• typeParams : Lean.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 : Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.Param

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.argToMono (arg : Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.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 : Lean.ConstructorVal) (args : Array Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.LetValue

Equations

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

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

def Lean.Compiler.LCNF.LetDecl.toMono (decl : Lean.Compiler.LCNF.LetDecl) : Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.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 : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.FunDecl

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

Convert cases Decidable => Bool

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

Eliminate cases for trivial structure. See hasTrivialStructure?

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

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

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.toMono : Lean.Compiler.LCNF.Pass

Equations

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