9.1. 声明结构体（Declaring Structures）9.1. Declaring Structures🔗

structure 命令本质上是一个用于定义归纳数据类型的"前端（front end）"。每个 structure 声明都会引入一个同名命名空间（namespace）。一般形式如下：The structure command is essentially a “front end” for defining inductive data types. Every structure declaration introduces a namespace with the same name. The general form is as follows:

    structure <name> <parameters> <parent-structures> where
      <constructor> :: <fields>

大多数部分是可选的。下面是一个例子：Most parts are optional. Here is an example:

类型 Point 的值使用 Point.mk a b 创建，点 p 的字段使用 Point.x p 和 Point.y p 访问（但 p.x 和 p.y 也可以，见下文）。structure 命令还会生成有用的递归子（recursor）和定理。以下是为上述声明生成的一些构造。Values of type Point are created using Point.mk a b, and the fields of a point p are accessed using Point.x p and Point.y p (but p.x and p.y also work, see below). The structure command also generates useful recursors and theorems. Here are some of the constructions generated for the declaration above.

Point.{u} (α : Type u) : Type u

@Point.rec : {α : Type u_2} →
  {motive : Point α → Sort u_1} → ((x y : α) → motive { x := x, y := y }) → (t : Point α) → motive t

@Point.mk : {α : Type u_1} → α → α → Point α

@Point.x : {α : Type u_1} → Point α → α

@Point.y : {α : Type u_1} → Point α → α

如果未提供构造器名称，则构造器默认命名为 mk。If the constructor name is not provided, then a constructor is named mk by default.

以下是一些使用所生成构造的简单定理和表达式。通常，你可以使用 open Point 命令来避免前缀 Point。Here are some simple theorems and expressions that use the generated constructions. As usual, you can avoid the prefix Point by using the command open Point.

10

20

给定 p : Point Nat，点表示法（dot notation）p.x 是 Point.x p 的简写。这提供了一种访问结构体字段的便捷方式。Given p : Point Nat, the dot notation p.x is shorthand for Point.x p. This provides a convenient way of accessing the fields of a structure.

p.x : Nat

10

20

点表示法不仅方便访问记录的投影，也方便应用在具有相同名称的命名空间中定义的函数。回顾合取（Conjunction）一节，如果 p 的类型是 Point，表达式 p.foo 被解释为 Point.foo p，前提是 foo 的第一个非隐式参数的类型为 Point。因此，在下面的例子中，表达式 p.add q 是 Point.add p q 的简写。The dot notation is convenient not just for accessing the projections of a record, but also for applying functions defined in a namespace with the same name. Recall from the Conjunction section if p has type Point, the expression p.foo is interpreted as Point.foo p, assuming that the first non-implicit argument to foo has type Point. The expression p.add q is therefore shorthand for Point.add p q in the example below.

{ x := 4, y := 6 }

在下一章中，你将学习如何定义像 add 这样的函数，使其适用于 Point α 的元素而不只是 Point Nat，前提是 α 具有关联的加法运算。In the next chapter, you will learn how to define a function like add so that it works generically for elements of Point α rather than just Point Nat, assuming α has an associated addition operation.

更一般地，给定表达式 p.foo x y z，其中 p : Point，Lean 会将 p 插入到 Point.foo 的第一个类型为 Point 的参数位置。例如，使用下面的标量乘法定义，p.smul 3 被解释为 Point.smul 3 p。More generally, given an expression p.foo x y z where p : Point, Lean will insert p at the first argument to Point.foo of type Point. For example, with the definition of scalar multiplication below, p.smul 3 is interpreted as Point.smul 3 p.

{ x := 3, y := 6 }

使用 List.map 函数（它将列表作为其第二个非隐式参数）采用类似的技巧是很常见的：It is common to use a similar trick with the List.map function, which takes a list as its second non-implicit argument:

@List.map : {α : Type u_1} → {β : Type u_2} → (α → β) → List α → List β

[1, 4, 9]

这里 xs.map f 被解释为 List.map f xs。Here xs.map f is interpreted as List.map f xs.

9.2. 对象（Objects）9.2. Objects🔗

我们一直在使用构造器来创建结构体类型的元素。对于包含许多字段的结构体来说，这通常很不方便，因为我们必须记住字段定义的顺序。因此，Lean 提供了以下替代表示法来定义结构体类型的元素。We have been using constructors to create elements of a structure type. For structures containing many fields, this is often inconvenient, because we have to remember the order in which the fields were defined. Lean therefore provides the following alternative notations for defining elements of a structure type.

    { (<field-name> := <expr>)* : structure-type }
    or
    { (<field-name> := <expr>)* }

后缀 : structure-type 可以在结构体名称能从期望类型推断出时省略。例如，我们使用这种表示法来定义"点"。字段指定的顺序无关紧要，因此下面的所有表达式都定义同一个点。The suffix : structure-type can be omitted whenever the name of the structure can be inferred from the expected type. For example, we use this notation to define “points.” The order that the fields are specified does not matter, so all the expressions below define the same point.

{ x := 10, y := 20 } : Point Nat

{ x := 10, y := 20 } : Point Nat

{ x := 10, y := 20 } : Point Nat

字段可以使用花括号标记为隐式（implicit）。隐式字段会成为构造器的隐式参数。Fields can be marked as implicit using curly braces. Implicit fields become implicit parameters to the constructor.

如果未指定字段的值，Lean 会尝试推断它。如果无法推断未指定的字段，Lean 会标记一个错误，指示相应的占位符无法被合成（synthesize）。If the value of a field is not specified, Lean tries to infer it. If the unspecified fields cannot be inferred, Lean flags an error indicating the corresponding placeholder could not be synthesized.

{ α := Nat, β := Bool, a := 10, b := true } : MyStruct

记录更新（record update）是另一种常见操作，即通过修改旧记录中一个或多个字段的值来创建新的记录对象。Lean 允许你通过添加注解 s with 到字段赋值之前，来指定记录的规范中未赋值的字段应从先前定义的结构体对象 s 中获取。如果提供了多个记录对象，则按顺序访问它们，直到 Lean 找到包含未指定字段的那个。如果在访问所有对象后仍有任何字段名未指定，Lean 会引发错误。Record update is another common operation which amounts to creating a new record object by modifying the value of one or more fields in an old one. Lean allows you to specify that unassigned fields in the specification of a record should be taken from a previously defined structure object s by adding the annotation s with before the field assignments. If more than one record object is provided, then they are visited in order until Lean finds one that contains the unspecified field. Lean raises an error if any of the field names remain unspecified after all the objects are visited.

{ x := 1, y := 3 }

{ x := 4, y := 2 }

9.3. 继承（Inheritance）9.3. Inheritance🔗

我们可以通过添加新字段来扩展（extend）现有结构体。这一特性使我们能够模拟一种继承（inheritance）。We can extend existing structures by adding new fields. This feature allows us to simulate a form of inheritance.

在下一个例子中，我们使用多重继承定义一个结构体，然后使用父结构体的对象来定义一个对象。In the next example, we define a structure using multiple inheritance, and then define an object using objects of the parent structures.