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 >> optional «extends» >> Term.optType >> optional (" := " >> optional structCtor >> structFields)

structure Lean.Elab.Command.StructFieldView : Type

• 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

  Same as name but includes macro scopes. Used 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 Syntax
• fields : Array StructFieldView

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 : StructView → CtorView

Equations

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

structure Lean.Elab.Command.StructParentInfo : Type

• ref : Syntax
• fvar? : Option Expr
• structName : Name
• subobject : Bool
• type : Expr

instance Lean.Elab.Command.instInhabitedStructParentInfo : Inhabited StructParentInfo

Equations

• Lean.Elab.Command.instInhabitedStructParentInfo = { default := { ref := default, fvar? := default, structName := default, subobject := default, type := default } }

inductive Lean.Elab.Command.StructFieldKind : Type

• newField : StructFieldKind
• copiedField : StructFieldKind
• fromParent : StructFieldKind
• subobject (structName : Name) : StructFieldKind

  The field is an embedded parent.

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

• ref : Syntax
• name : Name
• declName : Name

  Name of projection function. Remark: for fromParent fields, declName is only relevant in the generation of auxiliary "default value" functions.

• fvar : Expr
• kind : StructFieldKind
• value? : Option Expr

instance Lean.Elab.Command.instInhabitedStructFieldInfo : Inhabited StructFieldInfo

Equations

• Lean.Elab.Command.instInhabitedStructFieldInfo = { default := { ref := default, name := default, declName := default, fvar := default, kind := 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.isFromParent (info : StructFieldInfo) : Bool

Equations

• info.isFromParent = match info.kind with | Lean.Elab.Command.StructFieldKind.fromParent => 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

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.