总结
求值表达式
在 Lean 中，计算发生在求值表达式时。这遵循数学表达式的通常规则：
子表达式按照通常的运算顺序替换为其值，直到整个表达式变为一个值。
在求值 if 或 match 时，分支中的表达式不会被求值，直到找到条件为真或匹配主项的值。
变量一旦被赋予值，就不会再改变。这与数学类似，但与大多数编程语言不同，
Lean 变量只是值的占位符，而非可以写入新值的位置。变量的值可能来自带有
def 的全局定义、带有 let 的局部定义、作为函数的命名参数或模式匹配。
函数
Lean 中的函数是一等的值，这意味着它们可以作为参数传递给其他函数、
保存在变量中，并像任何其他值一样使用。每个 Lean 函数只接受一个参数。
为了对接受多个参数的函数进行编码，Lean 使用了一种称为 柯里化（Currying） 的技术，
其中提供第一个参数会返回一个期望剩余参数的函数。为了对不接受任何参数的函数进行编码，
Lean 使用了 Unit 类型，这是最没有信息量的可用参数。
创建函数的主要方式有三种：
- 匿名函数使用
fun编写。例如，一个交换Point字段的函数可以写成fun (point : Point) => { x := point.y, y := point.x : Point }。 - 非常简单的匿名函数通过在括号内放置一个或多个间点
·来编写。 每个间点都是函数的一个参数，用括号限定其主体。 例如，一个从其参数中减去 1 的函数可以写成(· - 1)而非fun x => x - 1。 - 函数可以用
def或let定义，方法是添加参数列表或使用模式匹配记法。
类型
Lean 会检查每个表达式是否具有类型。类型（例如 Int、Point、{α : Type} → Nat → α → List α
和 Option (String ⊕ (Nat × String))）描述了表达式最终可能求出的值。
与其他语言一样，Lean 中的类型可以表达由 Lean 编译器检查的程序的轻量级规范，
从而消除对具体的类进行单元测试的需求。与大多数语言不同，Lean 的类型还可以表示任意数学，
统一了编程和定理证明的世界。虽然将 Lean 用于定理证明在很大程度上超出了本书的范围，
但《Lean 4 定理证明》
一书中包含了有关该主题的更多信息。
某些表达式可被赋予多种类型。例如，3 可以是 Int 或 Nat。
在 Lean 中，这应该理解为两个独立的表达式，一个类型为 Nat，另一个类型为 Int，
只是它们碰巧以相同的方式编写，而非同一事物的两种不同类型。
Lean 有时能够自动确定类型，但类型通常必须由用户提供。
这是因为 Lean 的类型系统非常具有表现力。即使 Lean 可以找到一种类型，
它找到的也可能不是需要的类型。例如 3 可能打算用作 Int，但如果没有任何进一步的约束，
Lean 将赋予它 Nat 类型。一般来说，最好显式地写出大多数类型，
只让 Lean 填写非常明显的类型。这样能改进 Lean 的错误信息，并有助于使程序员的意图更加清晰。
某些函数或数据类型将类型作为参数。它们被称为 多态（Polymorphic） 。 多态性能让计算列表长度这类的程序不必关心列表中条目的具体类型。 由于类型在 Lean 中是一等公民，因此多态性不需要任何特殊语法，类型就能像其他参数一样传递。 在函数类型中为参数指定名称能让稍后的类型引用该参数， 并且通过将参数的名称替换为参数的值，就能知道应该将此函数应用于何种类型的参数。
结构体与归纳类型
可以使用 structure 或 inductive 特性向 Lean 引入全新的数据类型。
即使它们的定义在其他方面相同，这些新类型也不被认为等同于任何其他类型。
数据类型具有 构造子（Constructor） ，解释了可以构造其值的方式，
每个构造子都接受一些参数。Lean 中的构造子与面向对象语言中的构造函数不同：
Lean 的构造子只是数据的单纯持有者，而非初始化已分配对象的活动代码。
通常，structure 用于引入积类型（即，只有一个构造子且该构造子可以接受任意数量参数的类型），
而 inductive 用于引入和类型（即，具有多个不同构造子的类型）。
使用 structure 定义的数据类型会为构造子的每个参数提供一个访问器函数。
结构体和归纳数据类型都可以使用模式匹配来使用，
模式匹配使用调用所述构造子的语法的一个子集来表达存储在构造子中的值。
模式匹配意味着知道如何创建值就意味着知道如何使用它。
递归
当正在定义的名称在定义本身中使用时，定义就是递归的。 由于 Lean 除了是一种编程语言之外，还是一个交互式定理证明器， 因此对递归定义施加了某些限制。在 Lean 的逻辑方面，循环定义可能会导致逻辑不一致。
为确保递归定义的函数不会破坏 Lean 的逻辑方面，无论使用什么参数调它们， Lean 都必须能够证明所有函数都会停机。在实践中，这意味着递归调用都会在输入的结构中更小的部分上执行， 这确保了函数始终朝着基本情况推进，或者用户必须提供一些其他证据来证明函数必定会停机。 类似地，递归归纳类型不允许拥有 从类型中 接受一个函数作为参数的构造子， 因为这会让 Lean 能够编码不停机的函数。