opaque Lean.Elab.Command.structureDiamondWarning : Lean.Option Bool

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

Recall that the `structure command syntax is

leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> Term.optType >> optional «extends» >> optional (" := " >> optional structCtor >> structFields)

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

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

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

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

structure Lean.Elab.Command.Structure.StructViewextends 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
• parents : Array StructParentView
• fields : Array StructFieldView

Instances For

• Lean.Elab.Command.Structure.instInhabitedStructView

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

Equations

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

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

Gets the single constructor view from the underlying InductiveView. Recall that structures have exactly one constructor.

Equations

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

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

• Lean.Elab.Command.Structure.instInhabitedStructParentInfo

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

Equations

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

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

• Lean.Elab.Command.Structure.instInhabitedStructFieldKind
• Lean.Elab.Command.Structure.instReprStructFieldKind

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

Equations

• Lean.Elab.Command.Structure.instInhabitedStructFieldKind = { default := Lean.Elab.Command.Structure.StructFieldKind.newField }

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

Equations

• Lean.Elab.Command.Structure.instDecidableEqStructFieldKind = Lean.Elab.Command.Structure.decEqStructFieldKind✝

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

Equations

• Lean.Elab.Command.Structure.instReprStructFieldKind = { reprPrec := Lean.Elab.Command.Structure.reprStructFieldKind✝ }

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

Equations

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

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

Equations

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

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

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

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

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

Instances For

• Lean.Elab.Command.Structure.instReprStructFieldDefault

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

Equations

• Lean.Elab.Command.Structure.instReprStructFieldDefault = { reprPrec := Lean.Elab.Command.Structure.reprStructFieldDefault✝ }

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

• Lean.Elab.Command.Structure.instInhabitedStructFieldInfo

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

Equations

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

View construction

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

Equations

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

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.

Elaboration

instance Lean.Elab.Command.Structure.instInhabitedState : Inhabited Lean.Elab.Command.Structure.State✝

Equations

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

instance Lean.Elab.Command.Structure.instInhabitedStructElabM {α : Type} : Inhabited (Lean.Elab.Command.Structure.StructElabM✝ α)

Equations

• Lean.Elab.Command.Structure.instInhabitedStructElabM = { default := throw default }

def Lean.Elab.Command.Structure.runStructElabM {α : Type} (k : Lean.Elab.Command.Structure.StructElabM✝ α) (init : Lean.Elab.Command.Structure.State✝ := { }) : TermElabM α

Equations

• Lean.Elab.Command.Structure.runStructElabM k init = StateT.run' k init

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

Equations

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