Documentation

Lean.Elab.Structure

Recall that the `structure command syntax is

leading_parser (structureTk <|> classTk) >> declId >> optDeclSig >> 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
          Equations
          • One or more equations did not get rendered due to their size.
          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
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  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
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        View construction #

                        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

                            Elaboration #

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