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

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
Equations

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.

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.

• The LCNF type for the mono phase.

mono :

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
Equations
• One or more equations did not get rendered due to their size.