Recall that the `structure command syntax is
leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> optional (" := " >> optional structCtor >> structFields)
- ref : Lean.Syntax
- modifiers : Lean.Elab.Modifiers
- name : Lean.Name
- declName : Lean.Name
Instances For
Equations
- Lean.Elab.Command.instInhabitedStructCtorView = { default := { ref := default, modifiers := default, name := default, declName := default } }
- 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
Instances For
- ref : Lean.Syntax
- declId : Lean.Syntax
- modifiers : Lean.Elab.Modifiers
- isClass : Bool
- shortDeclName : Lean.Name
- declName : Lean.Name
- binders : Lean.Syntax
- type : Lean.Syntax
- parents : Array Lean.Syntax
- fields : Array Lean.Elab.Command.StructFieldView
- derivingClasses : Array Lean.Elab.DerivingClassView
Instances For
Equations
- One or more equations did not get rendered due to their size.
- ref : Lean.Syntax
- structName : Lean.Name
- subobject : Bool
- type : Lean.Expr
Instances For
Equations
- Lean.Elab.Command.instInhabitedStructParentInfo = { default := { ref := default, fvar? := default, structName := default, subobject := default, type := default } }
- 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.
Instances For
- 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
Instances For
Equations
- Lean.Elab.Command.instInhabitedStructFieldInfo = { default := { ref := default, name := default, declName := default, fvar := default, kind := default, value? := default } }
- view : Lean.Elab.Command.StructView
- lctx : Lean.LocalContext
- localInsts : Lean.LocalInstances
- type : Lean.Expr
- parents : Array Lean.Elab.Command.StructParentInfo
- parentFieldInfos : Array Lean.Elab.Command.StructFieldInfo
Field infos from parents.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- info.isFromParent = match info.kind with | Lean.Elab.Command.StructFieldKind.fromParent => true | x => false
Instances For
Equations
- info.isSubobject = match info.kind with | Lean.Elab.Command.StructFieldKind.subobject structName => true | x => false
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
Equations
Instances For
def
Lean.Elab.Command.mkStructureDecl
(vars : Array Lean.Expr)
(view : Lean.Elab.Command.StructView)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Elab.Command.elabStructureView
(vars : Array Lean.Expr)
(view : Lean.Elab.Command.StructView)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.