Documentation

Lean.Compiler.LCNF.Irrelevant

source
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.

Instances For
    source
    @[instance_reducible]
    instance Lean.Compiler.LCNF.instInhabitedTrivialStructureInfo :
    Inhabited TrivialStructureInfo
    source
    @[instance_reducible]
    instance Lean.Compiler.LCNF.instReprTrivialStructureInfo :
    Repr TrivialStructureInfo
    source
    def Lean.Compiler.LCNF.instReprTrivialStructureInfo.repr :
    TrivialStructureInfo → Nat → Format
    Instances For
      source
      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.

      Instances For
        source
        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.

        Instances For