Documentation

Lean.Compiler.LCNF.MonoTypes

Given a constructor, return a bitmask m s.t. m[i] is true if field i is computationally relevant.

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

    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

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

        Convert a LCNF type from the base phase to the mono phase.

        LCNF types in the mono phase do not have dependencies, and universe levels have been erased.

        The type contains only and constants.

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

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