Documentation

Lean.Elab.Structure

Recall that the `structure command syntax is

leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> Term.optType >> optional «extends» >> optional (" := " >> optional structCtor >> structFields)

Represents the data of the syntax of a structure parent.

  • ref : Syntax
  • projRef : Syntax

    Ref to use for the parent projection.

  • name? : Option Name

    The name of the parent projection (without macro scopes).

  • rawName? : Option Name

    The name of the parent projection (with macro scopes). Used for local name during elaboration.

  • type : Syntax
Instances For

    Represents the data of the syntax of a structure field declaration.

    Instances For

      Gets the single constructor view from the underlying InductiveView. Recall that structures have exactly one constructor.

      Equations
        Instances For

          Elaborated parent info.

          • ref : Syntax
          • addTermInfo : Bool

            Whether to add term info to the ref. False if there's no user-provided parent projection.

          • fvar : Expr

            A let variable that represents this structure parent.

          • structName : Name
          • name : Name

            Field name for parent.

          • declName : Name

            Name of the projection function.

          • subobject : Bool

            Whether this parent corresponds to a subobject field.

          Instances For

            Records the way in which a field is represented in a structure.

            Standard fields are one of .newField, .copiedField, or .fromSubobject. Parent fields are one of .subobject or .otherParent.

            • newField : StructFieldKind

              New field defined by the structure. Represented as a constructor argument. Will have a projection function.

            • copiedField : StructFieldKind

              Field that comes from a parent but will be represented as a new field. Represented as a constructor argument. Will have a projection function. Its inherited default value may be overridden.

            • fromSubobject : StructFieldKind

              Field that comes from a embedded parent field, and is represented within a subobject field. Not represented as a constructor argument. Will not have a projection function. Its inherited default value may be overridden.

            • subobject (structName : Name) : StructFieldKind

              The field is an embedded parent structure. Represented as a constructor argument. Will have a projection function. Default values are not allowed.

            • otherParent (structName : Name) : StructFieldKind

              The field represents a parent projection for a parent that is not itself embedded as a subobject. (Note: parents of subobject fields are otherParent fields.) Not represented as a constructor argument. Will only have a projection function if it is a direct parent. Default values are not allowed.

            Instances For

              Returns true if the field represents a parent projection.

              Equations
                Instances For

                  Returns true if the field is represented as a field in the constructor.

                  Equations
                    Instances For
                      Instances For

                        Elaborated field info.

                        • ref : Syntax
                        • name : Name
                        • declName : Name

                          Name of projection function. Remark: for fields that don't get projection functions (like fromSubobject fields), only relevant for the auxiliary "default value" functions.

                        • binfo : BinderInfo

                          Binder info to use when making the constructor. Only applies to those fields that will appear in the constructor.

                        • paramInfoOverrides : ExprMap (Syntax × BinderInfo)

                          Overrides for the parameters' binder infos when making the projections. The first component is a ref for the binder.

                        • sourceStructNames : List Name

                          Structure names that are responsible for this field being here.

                          • Empty if the field is a newField.
                          • Otherwise, it is a stack with the last element being a parent in the extends clause. The first element is the (indirect) parent that is responsible for this field.
                        • fvar : Expr

                          Local variable for the field. All fields (both real fields and parent projection fields) get a local variable. Parent fields are ldecls constructed from non-parent fields.

                        • projExpr? : Option Expr

                          An expression representing a .fromSubobject field as a projection of a .subobject field. Used when making the constructor. Note: .otherParent fields are let decls, there is no need for projExpr?.

                        • The default value, as explicitly given in this structure.

                        • projFn? : Option Name

                          If this is an inherited field, the name of the projection function. Used for adding terminfo for fields with overridden default values.

                        • inheritedDefaults : Array (Name × StructFieldDefault)

                          The inherited default values, as parent structure / value pairs.

                        • resolvedDefault? : Option StructFieldDefault

                          The default that will be used for this structure.

                        Instances For

                          View construction #

                          Elaboration #