- fieldName : Lake.Name
- projFn : Lake.Name
It is
some parentStructName
if it is a subobject, andparentStructName
is the name of the parent structure- binderInfo : Lean.BinderInfo
Instances For
Equations
- Lean.instInhabitedStructureFieldInfo = { default := { fieldName := default, projFn := default, subobject? := default, binderInfo := default, autoParam? := default } }
Equations
- Lean.instReprStructureFieldInfo = { reprPrec := Lean.reprStructureFieldInfo✝ }
Equations
- Lean.StructureFieldInfo.lt i₁ i₂ = Lean.Name.quickLt i₁.fieldName i₂.fieldName
Instances For
- structName : Lake.Name
- fieldInfo : Array Lean.StructureFieldInfo
Instances For
Equations
- Lean.instInhabitedStructureInfo = { default := { structName := default, fieldNames := default, fieldInfo := default } }
Equations
- Lean.StructureInfo.lt i₁ i₂ = Lean.Name.quickLt i₁.structName i₂.structName
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.instInhabitedStructureState = { default := { map := default } }
- structName : Lake.Name
- fields : Array Lean.StructureFieldInfo
Instances For
Equations
- Lean.instInhabitedStructureDescr = { default := { structName := default, fields := default } }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Get direct field names for the given structure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
If fieldName
represents the relation to a parent structure S
, return S
Equations
- Lean.isSubobjectField? env structName fieldName = match Lean.getFieldInfo? env structName fieldName with | some fieldInfo => fieldInfo.subobject? | x => none
Instances For
Return immediate parent structures
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return all parent structures
Equations
- Lean.getAllParentStructures env structName = (StateT.run (Lean.getAllParentStructures.visit env structName) #[]).snd
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.
Equations
- Lean.getStructureFieldsFlattened env structName includeSubobjectFields = Lean.getStructureFieldsFlattenedAux env structName #[] includeSubobjectFields
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.
Equations
- Lean.isStructure env constName = Option.isSome (Lean.getStructureInfo? env constName)
Instances For
Equations
- Lean.getProjFnForField? env structName fieldName = match Lean.getFieldInfo? env structName fieldName with | some fieldInfo => some fieldInfo.projFn | x => none
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.mkDefaultFnOfProjFn projFn = projFn ++ `_default
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
If baseStructName
is an ancestor structure for structName
, then return a sequence of projection functions
to go from structName
to baseStructName
.
Equations
- Lean.getPathToBaseStructure? env baseStructName structName = Lean.getPathToBaseStructureAux env baseStructName structName []
Instances For
Return true iff constName
is the a non-recursive inductive datatype that has only one constructor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return number of fields for a structure-like type
Equations
- One or more equations did not get rendered due to their size.