def Lean.Compiler.LCNF.setHasTrivialStructure? (declName : Name) : CoreM Unit

Eagerly computes and persists the trivial-structure info of declName; see compileDecls.

Equations

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

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.

Requires compileDecls to have been run for inductive declName.

Equations

• Lean.Compiler.LCNF.hasTrivialStructure? declName = Lean.Compiler.LCNF.Irrelevant.hasTrivialStructure? Lean.Compiler.LCNF.trivialStructureInfoExt✝ declName

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 : MapDeclarationExtension 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.setOtherDeclMonoType (declName : Name) : CoreM Unit

Eagerly computes and persists the mono type of declName; see compileDecls.

Equations

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

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

Returns the LCNF mono-phase type of declName, a declaration without associated code (constructor, inductive type, foreign function, or noncomputable definition).

Inductive types and their constructors are compiled eagerly by compileInductives (their mono type can depend on private constructor field types and so must be precomputed in the defining module); a miss for those is reported as an error. Other declarations have their mono type computed from the signature on demand and cached for the current module.

Equations

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