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

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

instance Lean.Compiler.LCNF.instReprTrivialStructureInfo : Repr TrivialStructureInfo

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

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.