函数类型是 Lean 的内置功能。 Functions 将一种类型 (domain) 的值映射到另一种类型 (codomain) 的值，function types 指定函数的域和余域。
函数类型有两种：
依赖函数类型显式命名参数，并且函数的共域可以显式引用该名称。 由于类型可以根据值计算，因此依赖函数可以返回任意数量的不同类型的值，具体取决于其参数。依赖函数有时称为 dependent products，因为它们对应于集合的索引乘积。
非依赖函数类型不包含参数名称，并且陪域不会根据提供的特定参数而变化。
函数 two 返回不同类型的值，具体取决于使用哪个参数调用它：
def two : (b : Bool) → if b then Unit × Unit else String :=
fun b =>
match b with
| true => ((), ())
| false => "two"
函数体不能用 if...then...else... 编写，因为它不像 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match 那样细化类型。
在Lean的核心语言中，所有函数类型都是相关的：非相关函数类型是参数名称不出现在codomain中的相关函数类型。 此外，如果重命名参数使它们相等，则具有不同参数名称的两个从属函数类型在定义上可能相等。 但是，Lean精化器不会引入非相关函数参数的本地绑定。
虽然核心 类型论 不具有 隐式 参数，但函数类型确实包含参数是否隐式的指示。 该信息由 Lean精化器使用，但它不会影响核心理论中的类型检查或 定义等价，并且在仅考虑核心 类型论 时可以忽略。
在 Lean 的 类型论 中，函数是使用绑定变量的 函数抽象 创建的。 在各个社区中，函数抽象也称为 lambdas，因为 Alonzo Church 对它们的表示法，或者称为匿名函数，因为它们不需要在全局环境中使用名称来定义。 应用该函数时，通过 β-reduction 找到结果：用参数替换绑定变量。 在编译的代码中，这种情况严格发生：参数必须已经是一个值。 类型检查时，没有这样的限制； 定义等价 的方程理论允许任意项进行 β 约简。
在Lean的术语语言中，函数抽象可以采用多个参数或使用模式匹配。 这些功能被转换为核心语言中更简单的操作，其中所有函数抽象都只采用一个参数。 并非所有函数都源自抽象：类型构造函数、构造函数 和 递归函数 可能具有函数类型，但不能单独使用函数抽象来定义它们。
在 Lean 的核心 类型论 中，每个函数将 domain 的每个元素映射到 codomain 的单个元素。 换句话说，每个函数都只需要一个参数。 多参数函数是通过定义高阶函数来实现的，当提供第一个参数时，该函数将返回一个需要其余参数的新函数。 这种编码称为 currying，由 Haskell B. Curry 推广并命名。 Lean 用于定义函数、指定其类型并应用它们的语法会产生多参数函数的错觉，但精化的结果仅包含单参数函数。
Lean 中的函数 定义等价 是 intensional。 这意味着 定义等价 是按语法定义的，对绑定变量和 约简 进行模重命名。 对于第一个近似，这意味着如果两个函数实现相同的算法，则它们在定义上是相等的，而不是通常的数学相等概念，即如果它们将 domain 的相等元素映射到 codomain 的相等元素，则两个函数相等。
定义等价 由类型检查器使用，因此它的可预测性非常重要。 内涵相等的句法特征意味着检查它的算法是可以确定的。 检查外延相等性涉及证明关于函数相等性的本质上任意定理，并且没有明确的规范来检查它的算法。 这使得扩展相等对于类型检查器来说是一个糟糕的选择。 相反，函数外延性作为推理原理提供，在证明 命题 两个函数相等时可以调用该推理原理。
除了绑定变量的缩减和重命名之外，定义等价 还支持一种有限形式的外延性，称为 η-equivalence，其中函数等于其主体将其应用于参数的抽象。
给定类型为 (x : α) → β x 的 f，f 定义上等于 fun x => f x。
在推理函数时，定理 funext与某些内涵类型理论不同，funext 是 Lean 中的定理。可以证明 使用商类型. 或相应的策略funext 或 ext 可用于证明两个函数相等，如果它们将相等的输入映射到相等的输出。
funext.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : ∀ (x : α), f x = g x) : f = gfunext.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : ∀ (x : α), f x = g x) : f = g
Function extensionality. If two functions return equal results for all possible arguments, then they are equal.
It is called “extensionality” because it provides a way to prove two objects equal based on the properties of the underlying mathematical functions, rather than based on the syntax used to denote them. Function extensionality is a theorem that can be proved using quotient types.
可以使用 Lean.Parser.Command.declaration : commanddef 递归定义函数。
从 Lean 的逻辑角度来看，所有函数都是 total，这意味着它们在有限时间内将 domain 的每个元素映射到 codomain 的元素。有些编程语言社群以另一种含义使用 total 一词：若函数不会因未处理的情形而崩溃，则认为它是全函数，而忽略非终止。
Total 函数的值是为所有类型正确的参数定义的，并且它们不会由于模式匹配中缺少大小写而无法终止或崩溃。
虽然Lean的逻辑模型认为所有功能都是完整的，但Lean也是一种实用的编程语言，提供了某些“逃生舱口”。 尚未证明可以终止的函数仍然可以在 Lean 的逻辑中使用，只要它们的 codomain 被证明为非空。 这些函数被 Lean 的逻辑视为未解释的函数，并且它们的计算行为被忽略。 在编译代码中，这些函数的处理方式与其他函数一样。 其他功能可能被标记为不安全；这些功能对于 Lean 的逻辑根本不可用。 关于 部分和不安全函数定义 的部分包含有关使用递归函数进行编程的更多详细信息。
同样，在编译代码中应在运行时失败的操作（例如对数组的越界访问）只能在已知结果类型存在时使用。
这些操作会导致在 Lean 逻辑中任意选择该类型的居民（具体来说，是在类型的 Inhabited 实例中指定的居民）。
函数 thirdChar 提取数组的第三个元素，或者如果数组有两个或更少的元素，则会出现混乱：
def thirdChar (xs : Array Char) : Char := xs[2]!
#['!'] 和 #['-', 'x'] 的（不存在的）第三个元素是相等的，因为它们产生相同的任意选择的字符：
example : thirdChar #['!'] = thirdChar #['-', 'x'] := rfl
事实上，两者都等于 'A'，这恰好是 Char 的默认后备：
example : thirdChar #['!'] = 'A' := rfl
example : thirdChar #['-', 'x'] = 'A' := rfl
Function 命名空间包含用于处理函数的通用帮助程序。
Function composition, usually written with the infix operator ∘. A new function is created from
two existing functions, where one function's output is used as input to the other.
Examples:
Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]
(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]
Conventions for notations in identifiers:
The recommended spelling of ∘ in identifiers is comp.
The constant function that ignores its argument.
If a : α, then Function.const β a : β → α is the “constant function with value a”. For all
arguments b : β, Function.const β a b = a. It is often written directly as fun _ => a.
Examples:
Function.const Bool 10 true = 10
Function.const Bool 10 false = 10
Function.const String 10 "any string" = 10
Function.curry.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {φ : Sort u_3} : (α × β → φ) → α → β → φFunction.curry.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {φ : Sort u_3} : (α × β → φ) → α → β → φ
Transforms a function from pairs into an equivalent two-parameter function.
Examples:
Function.curry (fun (x, y) => x + y) 3 5 = 8
Function.curry Prod.swap 3 "five" = ("five", 3)
Function.uncurry.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {φ : Sort u_3} : (α → β → φ) → α × β → φFunction.uncurry.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {φ : Sort u_3} : (α → β → φ) → α × β → φ
Transforms a two-parameter function into an equivalent function from pairs.
Examples:
Function.uncurry List.drop (1, ["a", "b", "c"]) = ["b", "c"]
[("orange", 2), ("android", 3) ].map (Function.uncurry String.take) = ["or", "and"]
A function f : α → β is called injective if f x = f y implies x = y.
A function f : α → β is called surjective if every b : β is equal to f a
for some a : α.
LeftInverse g f means that g is a left inverse to f. That is, g ∘ f = id.
HasLeftInverse f means that f has an unspecified left inverse.
RightInverse g f means that g is a right inverse to f. That is, f ∘ g = id.
HasRightInverse f means that f has an unspecified right inverse.