1.3. 函数和定义🔗

在 Lean 中，定义使用 def 关键字引入。例如，要定义名称 hello 来引用字符串 "Hello"，请编写：

def hello := "Hello"

在 Lean 中，新名称使用冒号加等号运算符 := 而非 = 定义。这是因为 = 用于描述现有表达式之间的相等性，而使用两个不同的运算符有助于避免混淆。

在 hello 的定义中，表达式 "Hello" 足够简单，Lean 能够自动确定定义的类型。然而，大多数定义并不那么简单，因此通常需要添加类型。这可以通过在要定义的名称后使用冒号来完成：

def lean : String := "Lean"

现在名称已经定义，它们可以使用了，因此

"Hello Lean"#eval String.append hello (String.append " " lean)

输出

"Hello Lean"

在 Lean 中，定义的名称只能在其定义之后使用。

在很多语言中，函数定义的语法与其他值的不同。例如，Python 函数定义以 def 关键字开头，而其他定义则以等号定义。在 Lean 中，函数使用与其他值相同的 def 关键字定义。尽管如此，像 hello 这类的定义引入的名字会直接引用其值，而非每次调用一个零参函数返回等价的值。

1.3.1. 定义函数🔗

在 Lean 中有多种方法可以定义函数，最简单的方法是在定义的类型之前放置函数的参数，并用空格分隔。例如，可以编写一个将其参数加 1 的函数：

def add1 (n : Nat) : Nat := n + 1

使用 #eval 测试此函数会得到 8，符合预期：

8#eval add1 7

就像将函数应用于多个参数会用空格分隔一样，接受多个参数的函数定义也是在参数名与类型之间加上空格。函数 maximum 的结果等于其两个参数中最大的一个，它接受两个 Nat 参数 n 和 k，并返回一个 Nat。

def maximum (n : Nat) (k : Nat) : Nat :=
  if n < k then
    k
  else n

类似地，函数 spaceBetween 用空格连接两个字符串。

def spaceBetween (before : String) (after : String) : String :=
  String.append before (String.append " " after)

当向 maximum 这样的已定义函数提供参数时，其结果会首先用提供的值替换函数体中对应的参数名称，然后对产生的函数体求值。例如：

                maximum (5 + 8) (2 * 7)maximum 13 14if 13 < 14 then 14 else 1314

求值为自然数、整数和字符串的表达式具有表明其类型的类型（分别为 Nat、Int 和 String）。函数也是如此。一个接受 Nat 并返回 Bool 的函数类型为 Nat → Bool，而一个接受两个 Nat 并返回一个 Nat 的函数类型为 Nat → Nat → Nat。

作为特例，当函数的名称直接与 #check 一起使用时，Lean 会返回函数的签名。输入 #check add1 会得到 add1 (n : Nat) : Nat。然而，Lean 可以通过将函数名称写在括号中来“欺骗”它显示函数的类型，这会导致函数被视为普通表达式，因此 #check (add1) 会得到 add1 : Nat → Nat，而 #check (maximum) 会得到 maximum : Nat → Nat → Nat。这个箭头也可以用 ASCII 替代箭头 -> 来写，因此前面的函数类型可以分别写成 example : Nat -> Nat := add1 和 example : Nat -> Nat -> Nat := maximum。

在幕后，所有函数实际上都只接受一个参数。像 maximum 这样看起来接受多个参数的函数，实际上是接受一个参数然后返回一个新函数。这个新函数接受下一个参数，并且这个过程会一直持续到不再需要更多参数为止。这可以通过向多参数函数提供一个参数来观察：#check maximum 3 会得到 maximum 3 : Nat → Nat，而 #check spaceBetween "Hello " 会得到 spaceBetween "Hello " : String → String。使用返回函数的函数来实现多参数函数被称为 柯里化，以数学家 Haskell Curry 命名。函数箭头是右结合的，这意味着 Nat → Nat → Nat 应该用括号括起来写成 Nat → (Nat → Nat)。

1.3.1.1. 练习🔗

定义一个函数 joinStringsWith，类型为 String → String → String → String，它通过将第一个参数放在第二个和第三个参数之间创建一个新的字符串。joinStringsWith ", " "one" "and another" 应该求值为 "one, and another"。
joinStringsWith ": " 的类型是什么？用 Lean 检查你的答案。
定义一个函数 volume，类型为 Nat → Nat → Nat → Nat，它计算给定高度、宽度和深度的长方体的体积。

1.3.2. 定义类型🔗

大多数类型化编程语言都有某种定义类型别名的方法，例如 C 语言的 typedef。然而，在 Lean 中，类型是语言的一等公民——它们像任何其他表达式一样。这意味着定义可以引用类型，就像它们可以引用其他值一样。

例如，如果 String 太长，可以定义一个更短的缩写 Str：

def Str : Type := String

然后可以使用 Str 作为定义的类型，而不是 String：

def aStr : Str := "This is a string."

这之所以有效，是因为类型遵循 Lean 的其余规则。类型是表达式，在表达式中，定义的名称可以替换为其定义。因为 Str 被定义为 String，所以 aStr 的定义是有意义的。

1.3.2.1. 你可能遇到的消息🔗

由于 Lean 支持重载整数文字的方式，尝试使用类型定义变得更加复杂。如果 Nat 太短，可以定义一个更长的名称 NaturalNumber：

def NaturalNumber : Type := Nat

然而，使用 NaturalNumber 作为定义的类型而不是 Nat 并不会产生预期的效果。特别是，定义：

def thirtyEight : NaturalNumber := failed to synthesize
  OfNat NaturalNumber 38
numerals are polymorphic in Lean, but the numeral `38` cannot be used in a context where the expected type is
  NaturalNumber
due to the absence of the instance above

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.38

导致以下错误：

failed to synthesize
  OfNat NaturalNumber 38
numerals are polymorphic in Lean, but the numeral `38` cannot be used in a context where the expected type is
  NaturalNumber
due to the absence of the instance above

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

此错误发生是因为 Lean 允许数字字面量被重载。当有意义时，自然数字面量可以用于新类型，就像这些类型是内置到系统中一样。这是 Lean 使数学表示方便的使命的一部分，而数学的不同分支使用数字表示法用于非常不同的目的。允许这种重载的特定功能在查找重载之前不会用它们的定义替换所有定义的名称，这就是导致上述错误消息的原因。

解决此限制的一种方法是在定义的右侧提供类型 Nat，从而使 Nat 的重载规则用于 38：

def thirtyEight : NaturalNumber := (38 : Nat)

该定义仍然是类型正确的，因为 NaturalNumber 与 Nat 是相同的类型——根据定义！

另一种解决方案是为 NaturalNumber 定义一个重载，其工作方式与 Nat 的重载等效。然而，这需要 Lean 更高级的功能。

最后，使用 abbrev 而非 def 为 Nat 定义新名称，允许重载解析用其定义替换定义的名称。使用 abbrev 编写的定义总是展开的。例如，

abbrev N : Type := Nat

和

def thirtyNine : N := 39

被接受，没有问题。

在幕后，一些定义在重载解析期间被内部标记为可展开，而另一些则不被标记。要展开的定义称为 可归约的。对可归约性的控制对于 Lean 的扩展至关重要：完全展开所有定义可能导致非常大的类型，这些类型机器处理起来很慢，用户也难以理解。使用 abbrev 生成的定义被标记为可归约的。