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

structure Lean.Elab.Command.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
• value? : Option Syntax

structure Lean.Elab.Command.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.instInhabitedStructView

instance Lean.Elab.Command.instInhabitedStructView : Inhabited StructView

Equations

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

def Lean.Elab.Command.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.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? : Option 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.

• type : Expr

Instances For

• Lean.Elab.Command.instInhabitedStructParentInfo

instance Lean.Elab.Command.instInhabitedStructParentInfo : Inhabited StructParentInfo

Equations

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

inductive Lean.Elab.Command.StructFieldKind : Type

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

• newField : StructFieldKind

  New field defined by this structure. The field is represented as a constructor argument.

• copiedField : StructFieldKind

  Field that comes from a parent but will be represented as a new field. The field is represented as a constructor argument. Its default value may be overridden.

• fromSubobject : StructFieldKind

  Field that comes from a embedded parent field, and is represented within a subobject field. Its default value may be overridden.

• subobject (structName : Name) : StructFieldKind

  The field is an embedded parent structure.

Instances For

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

instance Lean.Elab.Command.instInhabitedStructFieldKind : Inhabited StructFieldKind

Equations

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

instance Lean.Elab.Command.instDecidableEqStructFieldKind : DecidableEq StructFieldKind

Equations

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

instance Lean.Elab.Command.instReprStructFieldKind : Repr StructFieldKind

Equations

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

structure Lean.Elab.Command.StructFieldInfo : Type

Elaborated field info.

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

  Name of projection function. Remark: for fromSubobject fields, declName is only relevant for auxiliary "default value" functions.

• fvar : Expr
• value? : Option Expr

Instances For

• Lean.Elab.Command.instInhabitedStructFieldInfo
• Lean.Elab.Command.instReprStructFieldInfo

instance Lean.Elab.Command.instInhabitedStructFieldInfo : Inhabited StructFieldInfo

Equations

• Lean.Elab.Command.instInhabitedStructFieldInfo = { default := { ref := default, name := default, kind := default, declName := default, fvar := default, value? := default } }

instance Lean.Elab.Command.instReprStructFieldInfo : Repr StructFieldInfo

Equations

• Lean.Elab.Command.instReprStructFieldInfo = { reprPrec := Lean.Elab.Command.reprStructFieldInfo✝ }

def Lean.Elab.Command.StructFieldInfo.isFromSubobject (info : StructFieldInfo) : Bool

Equations

• info.isFromSubobject = match info.kind with | Lean.Elab.Command.StructFieldKind.fromSubobject => true | x => false

def Lean.Elab.Command.StructFieldInfo.isSubobject (info : StructFieldInfo) : Bool

Equations

• info.isSubobject = match info.kind with | Lean.Elab.Command.StructFieldKind.subobject structName => true | x => false

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev Lean.Elab.Command.FieldMap : Type

Map from field name to expression representing the field.

Equations

• Lean.Elab.Command.FieldMap = Lean.NameMap Lean.Expr

def Lean.Elab.Command.elabStructureCommand : InductiveElabDescr

Equations

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