structure Lean.Compiler.LCNF.OtherTypeExtState : Type

• The LCNF type for the base phase.

  base : Lean.PHashMap Lean.Name Lean.Expr

• The LCNF type for the mono phase.

  mono : Lean.PHashMap Lean.Name Lean.Expr

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

instance Lean.Compiler.LCNF.instInhabitedOtherTypeExtState : Inhabited Lean.Compiler.LCNF.OtherTypeExtState

Equations

• Lean.Compiler.LCNF.instInhabitedOtherTypeExtState = { default := { base := default, mono := default } }

opaque Lean.Compiler.LCNF.otherTypeExt : Lean.EnvExtension Lean.Compiler.LCNF.OtherTypeExtState

def Lean.Compiler.LCNF.getOtherDeclBaseType (declName : Lean.Name) (us : List Lean.Level) : Lean.CoreM Lean.Expr

Equations

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

def Lean.Compiler.LCNF.getOtherDeclType (declName : Lean.Name) (us : optParam (List Lean.Level) []) : Lean.Compiler.LCNF.CompilerM Lean.Expr

Return the LCNF type for constructors, inductive types, and foreign functions.

Equations

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