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.StructCtorView : Type

• ref : Lean.Syntax
• modifiers : Lean.Elab.Modifiers
• name : Lake.Name
• declName : Lake.Name

structure Lean.Elab.Command.StructFieldView : Type

• ref : Lean.Syntax
• modifiers : Lean.Elab.Modifiers
• binderInfo : Lean.BinderInfo
• declName : Lake.Name
• name : Lake.Name
• rawName : Lake.Name
• binders : Lean.Syntax
• type? : Option Lean.Syntax
• value? : Option Lean.Syntax

structure Lean.Elab.Command.StructView : Type

• ref : Lean.Syntax
• modifiers : Lean.Elab.Modifiers
• scopeLevelNames : List Lake.Name
• allUserLevelNames : List Lake.Name
• isClass : Bool
• declName : Lake.Name
• scopeVars : Array Lean.Expr
• params : Array Lean.Expr
• parents : Array Lean.Syntax
• type : Lean.Syntax
• ctor : Lean.Elab.Command.StructCtorView
• fields : Array Lean.Elab.Command.StructFieldView

inductive Lean.Elab.Command.StructFieldKind : Type

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

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

structure Lean.Elab.Command.StructFieldInfo : Type

• name : Lake.Name
• declName : Lake.Name
• 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

structure Lean.Elab.Command.ElabStructResult : Type (u_1 + 1)

• decl : Lean.Declaration
• projInfos : {ProjectionInfo : Type u_1} → List ProjectionInfo
• projInstances : List Lake.Name
• mctx : Lean.MetavarContext
• lctx : Lean.LocalContext
• localInsts : Lean.LocalInstances
• defaultAuxDecls : Array (Lake.Name × Lean.Expr × Lean.Expr)

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

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

@[inline, reducible]

abbrev Lean.Elab.Command.FieldMap : Type

def Lean.Elab.Command.elabStructure (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM Unit