Given a constructor, return a bitmask m
s.t. m[i]
is true if field i
is
computationally relevant.
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.
Instances For
Equations
- Lean.Compiler.LCNF.getParamTypes.go (Lean.Expr.forallE binderName d b binderInfo) r = Lean.Compiler.LCNF.getParamTypes.go b (Array.push r d)
- Lean.Compiler.LCNF.getParamTypes.go type r = r
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.
- mono : Lean.PHashMap Lake.Name Lean.Expr
The LCNF type for the
mono
phase.
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.