Given a structure S
, Lean automatically creates an auxiliary definition (projection function)
for each field. This structure caches information about these auxiliary definitions.
- ctorName : Name
Constructor associated with the auxiliary projection function.
- numParams : Nat
Number of parameters in the structure
- i : Nat
The field index associated with the auxiliary projection function.
- fromClass : Bool
true
if the structure is a class.
Instances For
@[export lean_mk_projection_info]
Equations
Instances For
@[export lean_projection_info_from_class]
Equations
Instances For
@[export lean_add_projection_info]
def
Lean.addProjectionFnInfo
(env : Environment)
(projName ctorName : Name)
(numParams i : Nat)
(fromClass : Bool)
:
Equations
Instances For
@[export lean_get_projection_info]
Equations
Instances For
Equations
Instances For
If projName
is the name of a projection function, return the associated structure name