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

Equations

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

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

Equations

• Lean.Elab.Command.instDecidableEqStructFieldKind x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

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

• 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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

@[reducible, inline]

abbrev Lean.Elab.Command.FieldMap : Type

Equations

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

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

Equations

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