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.ExprThe LCNF type for the monophase.
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.