structure Lean.StructureFieldInfo : Type

• fieldName : Lake.Name
• projFn : Lake.Name
• subobject? : Option Lake.Name

  It is some parentStructName if it is a subobject, and parentStructName is the name of the parent structure

• binderInfo : Lean.BinderInfo
• autoParam? : Option Lean.Expr

instance Lean.instInhabitedStructureFieldInfo : Inhabited Lean.StructureFieldInfo

Equations

• Lean.instInhabitedStructureFieldInfo = { default := { fieldName := default, projFn := default, subobject? := default, binderInfo := default, autoParam? := default } }

instance Lean.instReprStructureFieldInfo : Repr Lean.StructureFieldInfo

Equations

• Lean.instReprStructureFieldInfo = { reprPrec := Lean.reprStructureFieldInfo✝ }

def Lean.StructureFieldInfo.lt (i₁ : Lean.StructureFieldInfo) (i₂ : Lean.StructureFieldInfo) : Bool

Equations

• Lean.StructureFieldInfo.lt i₁ i₂ = Lean.Name.quickLt i₁.fieldName i₂.fieldName

structure Lean.StructureInfo : Type

• structName : Lake.Name
• fieldNames : Array Lake.Name
• fieldInfo : Array Lean.StructureFieldInfo

instance Lean.instInhabitedStructureInfo : Inhabited Lean.StructureInfo

Equations

• Lean.instInhabitedStructureInfo = { default := { structName := default, fieldNames := default, fieldInfo := default } }

def Lean.StructureInfo.lt (i₁ : Lean.StructureInfo) (i₂ : Lean.StructureInfo) : Bool

Equations

• Lean.StructureInfo.lt i₁ i₂ = Lean.Name.quickLt i₁.structName i₂.structName

def Lean.StructureInfo.getProjFn? (info : Lean.StructureInfo) (i : Nat) : Option Lake.Name

Equations

• One or more equations did not get rendered due to their size.

instance Lean.instInhabitedStructureState : Inhabited Lean.StructureState

Equations

• Lean.instInhabitedStructureState = { default := { map := default } }

opaque Lean.structureExt : Lean.SimplePersistentEnvExtension Lean.StructureInfo Lean.StructureState

structure Lean.StructureDescr : Type

• structName : Lake.Name
• fields : Array Lean.StructureFieldInfo

instance Lean.instInhabitedStructureDescr : Inhabited Lean.StructureDescr

Equations

• Lean.instInhabitedStructureDescr = { default := { structName := default, fields := default } }

def Lean.registerStructure (env : Lean.Environment) (e : Lean.StructureDescr) : Lean.Environment

Equations

• One or more equations did not get rendered due to their size.

def Lean.getStructureInfo? (env : Lean.Environment) (structName : Lake.Name) : Option Lean.StructureInfo

Equations

• One or more equations did not get rendered due to their size.

def Lean.getStructureCtor (env : Lean.Environment) (constName : Lake.Name) : Lean.ConstructorVal

Equations

• One or more equations did not get rendered due to their size.

def Lean.getStructureFields (env : Lean.Environment) (structName : Lake.Name) : Array Lake.Name

Get direct field names for the given structure.

Equations

• One or more equations did not get rendered due to their size.

def Lean.getFieldInfo? (env : Lean.Environment) (structName : Lake.Name) (fieldName : Lake.Name) : Option Lean.StructureFieldInfo

Equations

• One or more equations did not get rendered due to their size.

def Lean.isSubobjectField? (env : Lean.Environment) (structName : Lake.Name) (fieldName : Lake.Name) : Option Lake.Name

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

def Lean.getParentStructures (env : Lean.Environment) (structName : Lake.Name) : Array Lake.Name

Return immediate parent structures

Equations

• One or more equations did not get rendered due to their size.

def Lean.getAllParentStructures (env : Lean.Environment) (structName : Lake.Name) : Array Lake.Name

Return all parent structures

Equations

• Lean.getAllParentStructures env structName = (StateT.run (Lean.getAllParentStructures.visit env structName) #[]).snd

partial def Lean.getAllParentStructures.visit (env : Lean.Environment) (structName : Lake.Name) : StateT (Array Lake.Name) Id Unit

partial def Lean.findField? (env : Lean.Environment) (structName : Lake.Name) (fieldName : Lake.Name) : Option Lake.Name

findField? env S fname. If fname is defined in a parent S' of S, return S'

def Lean.getStructureFieldsFlattened (env : Lean.Environment) (structName : Lake.Name) (includeSubobjectFields : optParam Bool true) : Array Lake.Name

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

def Lean.isStructure (env : Lean.Environment) (constName : Lake.Name) : Bool

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)

def Lean.getProjFnForField? (env : Lean.Environment) (structName : Lake.Name) (fieldName : Lake.Name) : Option Lake.Name

Equations

• Lean.getProjFnForField? env structName fieldName = match Lean.getFieldInfo? env structName fieldName with | some fieldInfo => some fieldInfo.projFn | x => none

def Lean.getProjFnInfoForField? (env : Lean.Environment) (structName : Lake.Name) (fieldName : Lake.Name) : Option (Lake.Name × Lean.ProjectionFunctionInfo)

Equations

• One or more equations did not get rendered due to their size.

def Lean.mkDefaultFnOfProjFn (projFn : Lake.Name) : Lake.Name

Equations

• Lean.mkDefaultFnOfProjFn projFn = projFn ++ `_default

def Lean.getDefaultFnForField? (env : Lean.Environment) (structName : Lake.Name) (fieldName : Lake.Name) : Option Lake.Name

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.getPathToBaseStructureAux (env : Lean.Environment) (baseStructName : Lake.Name) (structName : Lake.Name) (path : List Lake.Name) : Option (List Lake.Name)

def Lean.getPathToBaseStructure? (env : Lean.Environment) (baseStructName : Lake.Name) (structName : Lake.Name) : Option (List Lake.Name)

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 []

def Lean.isStructureLike (env : Lean.Environment) (constName : Lake.Name) : Bool

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.

def Lean.getStructureLikeNumFields (env : Lean.Environment) (constName : Lake.Name) : Nat

Return number of fields for a structure-like type

Equations

• One or more equations did not get rendered due to their size.