Lean.Structure

source

structure Lean.StructureFieldInfo:

Type

fieldName : Lean.Name
projFn : Lean.Name
subobject? : Option Lean.Name
binderInfo : Lean.BinderInfo
autoParam? : Option Lean.Expr

source

instance Lean.instInhabitedStructureFieldInfo:

Inhabited Lean.StructureFieldInfo

Equations

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

source

instance Lean.instReprStructureFieldInfo:

Repr Lean.StructureFieldInfo

Equations

Lean.instReprStructureFieldInfo = { reprPrec := [anonymous] }

source

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

Bool

Equations

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

source

structure Lean.StructureInfo:

Type

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

source

instance Lean.instInhabitedStructureInfo:

Inhabited Lean.StructureInfo

Equations

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

source

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

Bool

Equations

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

source

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

Option Lean.Name

Equations

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

source

instance Lean.instInhabitedStructureState:

Inhabited Lean.StructureState

Equations

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

source

opaque Lean.structureExt:

Lean.SimplePersistentEnvExtension Lean.StructureInfo Lean.StructureState

source

structure Lean.StructureDescr:

Type

structName : Lean.Name
fields : Array Lean.StructureFieldInfo

source

instance Lean.instInhabitedStructureDescr:

Inhabited Lean.StructureDescr

Equations

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

source

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

Lean.Environment

Equations

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

source

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

Option Lean.StructureInfo

Equations

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

source

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

Lean.ConstructorVal

Equations

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

source

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

Array Lean.Name

Get direct field names for the given structure.

Equations

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

source

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

Option Lean.StructureFieldInfo

Equations

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

source

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

Option Lean.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

source

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

Array Lean.Name

Return immediate parent structures

Equations

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

source

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

Array Lean.Name

Return all parent structures

Equations

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

source

partial def Lean.getAllParentStructures.visit (env : Lean.Environment) (structName : Lean.Name) :

StateT (Array Lean.Name) Id Unit

source

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

Option Lean.Name

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

source

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

Array Lean.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

source

def Lean.isStructure (env : Lean.Environment) (constName : Lean.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)

source

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

Option Lean.Name

Equations

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

source

def Lean.getProjFnInfoForField? (env : Lean.Environment) (structName : Lean.Name) (fieldName : Lean.Name) :

Option (Lean.Name × Lean.ProjectionFunctionInfo)

Equations

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

source

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

Lean.Name

Equations

Lean.mkDefaultFnOfProjFn projFn = projFn ++ `_default

source

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

Option Lean.Name

Equations

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

source

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

Option (List Lean.Name)

source

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

Option (List Lean.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 []

source

def Lean.isStructureLike (env : Lean.Environment) (constName : Lean.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.

source

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

Nat

Return number of fields for a structure-like type

Equations

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