- fieldName : Lake.Name
- projFn : Lake.Name
It is
some parentStructNameif it is a subobject, andparentStructNameis the name of the parent structure- binderInfo : Lean.BinderInfo
Instances For
Instances For
- structName : Lake.Name
- fieldInfo : Array Lean.StructureFieldInfo
Instances For
Instances For
Instances For
- structName : Lake.Name
- fields : Array Lean.StructureFieldInfo
Instances For
Instances For
Instances For
Instances For
Get direct field names for the given structure.
Instances For
Instances For
If fieldName represents the relation to a parent structure S, return S
Instances For
Return immediate parent structures
Instances For
Return all parent structures
Instances For
findField? env S fname. If fname is defined in a parent S' of S, return S'
Return field names for the given structure, including "flattened" fields from parent
structures. To omit toParent projections, set includeSubobjectFields := false.
For example, given Bar such that
structure Foo where a : Nat
structure Bar extends Foo where b : Nat
return #[toFoo,a,b] or #[a,b] with subobject fields omitted.
Instances For
Return true if constName is the name of an inductive datatype
created using the structure or class commands.
We perform the check by testing whether auxiliary projection functions have been created.
Instances For
Instances For
Instances For
Instances For
If baseStructName is an ancestor structure for structName, then return a sequence of projection functions
to go from structName to baseStructName.
Instances For
Return true iff constName is the a non-recursive inductive datatype that has only one constructor.
Instances For
Return number of fields for a structure-like type