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 Lean.Compiler.LCNF.instInhabitedTrivialStructureInfo : Inhabited TrivialStructureInfo

Equations

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

def Lean.Compiler.LCNF.instInhabitedTrivialStructureInfo.default : TrivialStructureInfo

Equations

• Lean.Compiler.LCNF.instInhabitedTrivialStructureInfo.default = { ctorName := default, numParams := default, fieldIdx := default }

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.hasTrivialStructure? (cacheExt : CacheExtension Name (Option TrivialStructureInfo)) (trivialType : Expr → MetaM Bool) (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.