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