def Lean.Compiler.LCNF.hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo)

Return some fieldIdx if declName is the name of an inductive datatype s.t.

• It does not have builtin support in the runtime.
• It has only one constructor.
• This constructor has only one computationally relevant field.

Equations

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

def Lean.Compiler.LCNF.getParamTypes (type : Expr) : Array Expr

Equations

• Lean.Compiler.LCNF.getParamTypes type = Lean.Compiler.LCNF.getParamTypes.go✝ type #[]

partial def Lean.Compiler.LCNF.toMonoType (type : Expr) : CoreM Expr

Convert a LCNF type from the base phase to the mono phase.

LCNF types in the mono phase do not have dependencies, and universe levels have been erased.

The type contains only → and constants.

opaque Lean.Compiler.LCNF.monoTypeExt : CacheExtension Name Expr

State for the environment extension used to save the LCNF mono phase type for declarations that do not have code associated with them. Example: constructors, inductive types, foreign functions.

def Lean.Compiler.LCNF.getOtherDeclMonoType (declName : Name) : CoreM Expr

Equations

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