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

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

instance Lean.Elab.Command.instInhabitedStructCtorView : Inhabited Lean.Elab.Command.StructCtorView

Equations

• Lean.Elab.Command.instInhabitedStructCtorView = { default := { ref := default, modifiers := default, name := default, declName := default } }

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

• ref : Lean.Syntax
• declId : Lean.Syntax
• modifiers : Lean.Elab.Modifiers
• isClass : Bool
• shortDeclName : Lean.Name
• declName : Lean.Name
• levelNames : List Lean.Name
• binders : Lean.Syntax
• type : Lean.Syntax
• parents : Array Lean.Syntax
• ctor : Lean.Elab.Command.StructCtorView
• fields : Array Lean.Elab.Command.StructFieldView
• derivingClasses : Array Lean.Elab.DerivingClassView

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

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

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 = Lean.Elab.Command.decEqStructFieldKind✝

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

Equations

• Lean.Elab.Command.instInhabitedStructFieldInfo = { default := { ref := 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✝ }

structure Lean.Elab.Command.ElabStructHeaderResult : Type

• view : Lean.Elab.Command.StructView
• lctx : Lean.LocalContext
• localInsts : Lean.LocalInstances
• levelNames : List Lean.Name
• params : Array Lean.Expr
• type : Lean.Expr
• parents : Array Lean.Elab.Command.StructParentInfo
• parentFieldInfos : Array Lean.Elab.Command.StructFieldInfo

  Field infos from parents.

instance Lean.Elab.Command.instInhabitedElabStructHeaderResult : Inhabited Lean.Elab.Command.ElabStructHeaderResult

Equations

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

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

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.mkStructureDecl (vars : Array Lean.Expr) (view : Lean.Elab.Command.StructView) : Lean.Elab.TermElabM Unit

Equations

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

def Lean.Elab.Command.elabStructureView (vars : Array Lean.Expr) (view : Lean.Elab.Command.StructView) : Lean.Elab.TermElabM Unit

Equations

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

def Lean.Elab.Command.elabStructureViewPostprocessing (view : Lean.Elab.Command.StructView) : Lean.Elab.Command.CommandElabM Unit

Equations

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

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.