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

instance Lean.instReprStructureFieldInfo : Repr Lean.StructureFieldInfo

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

structure Lean.StructureInfo : Type

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

instance Lean.instInhabitedStructureInfo : Inhabited Lean.StructureInfo

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

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

instance Lean.instInhabitedStructureState : Inhabited Lean.StructureState

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

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

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

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

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

Get direct field names for the given structure.

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

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

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

Return immediate parent structures

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

Return all parent structures

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.

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.

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

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

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

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

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.

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.

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

Return number of fields for a structure-like type