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 : Lean.Syntax
• modifiers : Lean.Elab.Modifiers
• binderInfo : Lean.BinderInfo
• declName : Lean.Name
• nameId : Lean.Syntax

  Ref for the field name

• name : Lean.Name

  The name of the field. (Without macro scopes.)

• rawName : Lean.Name

  Same as name but includes macro scopes. Used for field elaboration.

• binders : Lean.Syntax
• type? : Option Lean.Syntax
• value? : Option Lean.Syntax

structure Lean.Elab.Command.StructViewextends Lean.Elab.Command.InductiveView : Type

• ref : Lean.Syntax
• declId : Lean.Syntax
• modifiers : Lean.Elab.Modifiers
• isClass : Bool
• allowIndices : Bool
• allowSortPolymorphism : Bool
• shortDeclName : Lean.Name
• declName : Lean.Name
• levelNames : List Lean.Name
• binders : Lean.Syntax
• type? : Option Lean.Syntax
• ctors : Array Lean.Elab.Command.CtorView
• computedFields : Array Lean.Elab.Command.ComputedFieldView
• derivingClasses : Array Lean.Elab.DerivingClassView
• parents : Array Lean.Syntax
• fields : Array Lean.Elab.Command.StructFieldView

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

Equations

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

def Lean.Elab.Command.StructView.ctor : Lean.Elab.Command.StructView → Lean.Elab.Command.CtorView

Equations

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

structure Lean.Elab.Command.StructParentInfo : Type

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

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

Equations

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

inductive Lean.Elab.Command.StructFieldKind : Type

• newField: Lean.Elab.Command.StructFieldKind
• copiedField: Lean.Elab.Command.StructFieldKind
• fromParent: Lean.Elab.Command.StructFieldKind
• subobject: Lean.Name → Lean.Elab.Command.StructFieldKind

  The field is an embedded parent.

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

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

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

Equations

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

structure Lean.Elab.Command.StructFieldInfo : Type

• ref : Lean.Syntax
• name : Lean.Name
• declName : Lean.Name

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

• fvar : Lean.Expr
• kind : Lean.Elab.Command.StructFieldKind
• value? : Option Lean.Expr

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

instance Lean.Elab.Command.instReprStructFieldInfo : Repr Lean.Elab.Command.StructFieldInfo

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

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

Equations

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

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

def Lean.Elab.Command.structureSyntaxToView (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.TermElabM Lean.Elab.Command.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 : Lean.Elab.Command.InductiveElabDescr