source
opaque Lean.Elab.Command.structureDiamondWarning :
Lean.Option Bool
source
opaque Lean.Elab.Command.structure.strictResolutionOrder :
Lean.Option Bool

Recall that the `structure command syntax is

    leading_parser (structureTk <|> classTk) >> declId >> optDeclSig >> optional «extends» >> optional (" := " >> optional structCtor >> structFields)

source
structure Lean.Elab.Command.Structure.StructParentView :
Type

Represents the data of the syntax of a structure parent.

- ref : Syntax
- projRef : Syntax

  Ref to use for the parent projection.

- name? : Option Name

  The name of the parent projection (without macro scopes).

- rawName? : Option Name

  The name of the parent projection (with macro scopes). Used for local name during elaboration.

- type : Syntax

Instances For

source
inductive Lean.Elab.Command.Structure.StructFieldViewDefault :
Type

- optParam (value : Syntax) : StructFieldViewDefault
- autoParam (tactic : Syntax) : StructFieldViewDefault

Instances For

source
structure Lean.Elab.Command.Structure.StructFieldView :
Type

Represents the data of the syntax of a structure field declaration.

- ref : Syntax
- modifiers : Modifiers
- binderInfo : BinderInfo
- declName : Name
- nameId : Syntax

  Ref for the field name

- name : Name

  The name of the field (without macro scopes).

- rawName : Name

  The name of the field (with macro scopes). Used when adding the field to the local context, for field elaboration.

- binders : Syntax
- type? : Option Syntax
- default? : Option StructFieldViewDefault

Instances For

source
structure Lean.Elab.Command.Structure.StructView extends Lean.Elab.Command.InductiveView :
Type

- ref : Syntax
- declId : Syntax
- modifiers : Modifiers
- isClass : Bool
- allowIndices : Bool
- allowSortPolymorphism : Bool
- shortDeclName : Name
- declName : Name
- levelNames : List Name
- binders : Syntax
- type? : Option Syntax
- ctors : Array CtorView
- computedFields : Array ComputedFieldView
- derivingClasses : Array DerivingClassView
- docString? : Option (TSyntax `Lean.Parser.Command.docComment × Bool)
- isCoinductive : Bool
- parents : Array StructParentView
- fields : Array StructFieldView

Instances For

source
def Lean.Elab.Command.Structure.instInhabitedStructView.default :
StructView
Equations

- Lean.Elab.Command.Structure.instInhabitedStructView.default = { toInductiveView := default, parents := default, fields := default }

Instances For

source
instance Lean.Elab.Command.Structure.instInhabitedStructView :
Inhabited StructView
Equations

- Lean.Elab.Command.Structure.instInhabitedStructView = { default := Lean.Elab.Command.Structure.instInhabitedStructView.default }

source
def Lean.Elab.Command.Structure.StructView.ctor (view : StructView) :
CtorView

Gets the single constructor view from the underlying `InductiveView`. Recall that `structure`s have exactly one constructor.

Equations

- view.ctor = view.ctors[0]!

Instances For

source
structure Lean.Elab.Command.Structure.StructParentInfo :
Type

Elaborated parent info.

- ref : Syntax
- addTermInfo : Bool

  Whether to add term info to the ref. False if there's no user-provided parent projection.

- fvar : Expr

  A let variable that represents this structure parent.

- structName : Name
- name : Name

  Field name for parent.

- declName : Name

  Name of the projection function.

- subobject : Bool

  Whether this parent corresponds to a `subobject` field.

Instances For

source
def Lean.Elab.Command.Structure.instInhabitedStructParentInfo.default :
StructParentInfo
Equations

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

Instances For

source
instance Lean.Elab.Command.Structure.instInhabitedStructParentInfo :
Inhabited StructParentInfo
Equations

- Lean.Elab.Command.Structure.instInhabitedStructParentInfo = { default := Lean.Elab.Command.Structure.instInhabitedStructParentInfo.default }

source
inductive Lean.Elab.Command.Structure.StructFieldKind :
Type

Records the way in which a field is represented in a structure.

Standard fields are one of `.newField`, `.copiedField`, or `.fromSubobject`. Parent fields are one of `.subobject` or `.otherParent`.

- newField : StructFieldKind

  New field defined by the `structure`. Represented as a constructor argument. Will have a projection function.

- copiedField : StructFieldKind

  Field that comes from a parent but will be represented as a new field. Represented as a constructor argument. Will have a projection function. Its inherited default value may be overridden.

- fromSubobject : StructFieldKind

  Field that comes from a embedded parent field, and is represented within a `subobject` field. Not represented as a constructor argument. Will not have a projection function. Its inherited default value may be overridden.

- subobject (structName : Name) : StructFieldKind

  The field is an embedded parent structure. Represented as a constructor argument. Will have a projection function. Default values are not allowed.

- otherParent (structName : Name) : StructFieldKind

  The field represents a parent projection for a parent that is not itself embedded as a subobject. (Note: parents of `subobject` fields are `otherParent` fields.) Not represented as a constructor argument. Will only have a projection function if it is a direct parent. Default values are not allowed.

Instances For

source
def Lean.Elab.Command.Structure.instInhabitedStructFieldKind.default :
StructFieldKind
Equations

- Lean.Elab.Command.Structure.instInhabitedStructFieldKind.default = Lean.Elab.Command.Structure.StructFieldKind.newField

Instances For

source
instance Lean.Elab.Command.Structure.instInhabitedStructFieldKind :
Inhabited StructFieldKind
Equations

- Lean.Elab.Command.Structure.instInhabitedStructFieldKind = { default := Lean.Elab.Command.Structure.instInhabitedStructFieldKind.default }

source
instance Lean.Elab.Command.Structure.instDecidableEqStructFieldKind :
DecidableEq StructFieldKind
Equations

- Lean.Elab.Command.Structure.instDecidableEqStructFieldKind = Lean.Elab.Command.Structure.instDecidableEqStructFieldKind.decEq

source
def Lean.Elab.Command.Structure.instDecidableEqStructFieldKind.decEq (x✝ x✝¹ : StructFieldKind) :
Decidable (x✝ = x✝¹)
Equations

- One or more equations did not get rendered due to their size.
- Lean.Elab.Command.Structure.instDecidableEqStructFieldKind.decEq Lean.Elab.Command.Structure.StructFieldKind.newField Lean.Elab.Command.Structure.StructFieldKind.newField = isTrue ⋯
- Lean.Elab.Command.Structure.instDecidableEqStructFieldKind.decEq Lean.Elab.Command.Structure.StructFieldKind.copiedField Lean.Elab.Command.Structure.StructFieldKind.copiedField = isTrue ⋯

Instances For

source
instance Lean.Elab.Command.Structure.instReprStructFieldKind :
Repr StructFieldKind
Equations

- Lean.Elab.Command.Structure.instReprStructFieldKind = { reprPrec := Lean.Elab.Command.Structure.instReprStructFieldKind.repr }

source
def Lean.Elab.Command.Structure.instReprStructFieldKind.repr :
StructFieldKind → Nat → Format
Equations

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

Instances For

source
def Lean.Elab.Command.Structure.StructFieldKind.isFromSubobject (kind : StructFieldKind) :
Bool
Equations

- Lean.Elab.Command.Structure.StructFieldKind.fromSubobject.isFromSubobject = true
- kind.isFromSubobject = false

Instances For

source
def Lean.Elab.Command.Structure.StructFieldKind.isSubobject (kind : StructFieldKind) :
Bool
Equations

- (Lean.Elab.Command.Structure.StructFieldKind.subobject structName).isSubobject = true
- kind.isSubobject = false

Instances For

source
def Lean.Elab.Command.Structure.StructFieldKind.isParent (kind : StructFieldKind) :
Bool

Returns `true` if the field represents a parent projection.

Equations

- (Lean.Elab.Command.Structure.StructFieldKind.subobject structName).isParent = true
- (Lean.Elab.Command.Structure.StructFieldKind.otherParent structName).isParent = true
- kind.isParent = false

Instances For

source
def Lean.Elab.Command.Structure.StructFieldKind.isInCtor (kind : StructFieldKind) :
Bool

Returns `true` if the field is represented as a field in the constructor.

Equations

- Lean.Elab.Command.Structure.StructFieldKind.newField.isInCtor = true
- Lean.Elab.Command.Structure.StructFieldKind.copiedField.isInCtor = true
- (Lean.Elab.Command.Structure.StructFieldKind.subobject structName).isInCtor = true
- kind.isInCtor = false

Instances For

source
inductive Lean.Elab.Command.Structure.StructFieldDefault :
Type

- optParam (value : Expr) : StructFieldDefault
- autoParam (tactic : Expr) : StructFieldDefault

Instances For

source
def Lean.Elab.Command.Structure.instReprStructFieldDefault.repr :
StructFieldDefault → Nat → Format
Equations

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

Instances For

source
instance Lean.Elab.Command.Structure.instReprStructFieldDefault :
Repr StructFieldDefault
Equations

- Lean.Elab.Command.Structure.instReprStructFieldDefault = { reprPrec := Lean.Elab.Command.Structure.instReprStructFieldDefault.repr }

source
structure Lean.Elab.Command.Structure.StructFieldInfo :
Type

Elaborated field info.

- ref : Syntax
- name : Name
- kind : StructFieldKind
- declName : Name

  Name of projection function. Remark: for fields that don't get projection functions (like `fromSubobject` fields), only relevant for the auxiliary "default value" functions.

- binfo : BinderInfo

  Binder info to use when making the constructor. Only applies to those fields that will appear in the constructor.

- paramInfoOverrides : ExprMap (Syntax × BinderInfo)

  Overrides for the parameters' binder infos when making the projections. The first component is a ref for the binder.

- sourceStructNames : List Name

  Structure names that are responsible for this field being here.

  - Empty if the field is a `newField`.
  - Otherwise, it is a stack with the last element being a parent in the `extends` clause. The first element is the (indirect) parent that is responsible for this field.
- fvar : Expr

  Local variable for the field. All fields (both real fields and parent projection fields) get a local variable. Parent fields are ldecls constructed from non-parent fields.

- projExpr? : Option Expr

  An expression representing a `.fromSubobject` field as a projection of a `.subobject` field. Used when making the constructor. Note: `.otherParent` fields are let decls, there is no need for `projExpr?`.

- default? : Option StructFieldDefault

  The default value, as explicitly given in this `structure`.

- projFn? : Option Name

  If this is an inherited field, the name of the projection function. Used for adding terminfo for fields with overridden default values.

- inheritedDefaults : Array (Name × StructFieldDefault)

  The inherited default values, as parent structure / value pairs.

- resolvedDefault? : Option StructFieldDefault

  The default that will be used for this structure.

Instances For

source
def Lean.Elab.Command.Structure.instInhabitedStructFieldInfo.default :
StructFieldInfo
Equations

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

Instances For

source
instance Lean.Elab.Command.Structure.instInhabitedStructFieldInfo :
Inhabited StructFieldInfo
Equations

- Lean.Elab.Command.Structure.instInhabitedStructFieldInfo = { default := Lean.Elab.Command.Structure.instInhabitedStructFieldInfo.default }

### View construction #

source
def Lean.Elab.Command.Structure.checkValidFieldModifier (modifiers : Modifiers) :
TermElabM Unit
Equations

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

Instances For

source
def Lean.Elab.Command.Structure.structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) :
TermElabM StructView
Equations

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

Instances For

### Elaboration #

source
def Lean.Elab.Command.Structure.elabStructureCommand :
InductiveElabDescr
Equations

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

Instances For