structure Lean.Compiler.LCNF.TrivialStructureInfo : Type

We say a structure has a trivial structure if it has not builtin support in the runtime, it has only one constructor, and this constructor has only one relevant field.

• ctorName : Name
• numParams : Nat
• fieldIdx : Nat

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedTrivialStructureInfo : Inhabited TrivialStructureInfo

Equations

• Lean.Compiler.LCNF.instInhabitedTrivialStructureInfo = { default := Lean.Compiler.LCNF.instInhabitedTrivialStructureInfo.default }

@[instance_reducible]

instance Lean.Compiler.LCNF.instReprTrivialStructureInfo : Repr TrivialStructureInfo

Equations

• Lean.Compiler.LCNF.instReprTrivialStructureInfo = { reprPrec := Lean.Compiler.LCNF.instReprTrivialStructureInfo.repr }

def Lean.Compiler.LCNF.instReprTrivialStructureInfo.repr : TrivialStructureInfo → Nat → Format

Equations

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

def Lean.Compiler.LCNF.Irrelevant.setHasTrivialStructure? (infoExt : MapDeclarationExtension (Option TrivialStructureInfo)) (trivialType : Expr → MetaM Bool) (declName : Name) : CoreM Unit

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

Equations

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

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

Trivial-structure info for declName (none for non-inductives); requires compileDecls to have been run for inductive declName.

Equations

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