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

                    Equations
                      Instances For