最基本的函数抽象引入一个变量来代表函数的参数：
term ::= ... | fun ident => term
在精化时间，Lean 必须能够确定函数的域。 类型归属是提供此信息的一种方式：
term ::= ... | fun ident : term => term
13.3. 功能
具有函数类型的术语可以通过抽象创建，通过 Lean.Parser.Term.fun : termfun 关键字引入。在各个社区中，函数抽象也称为 lambdas，因为 Alonzo Church 对它们的表示法，或者称为匿名函数，因为它们不需要在全局环境中使用名称进行定义。
虽然核心 类型论 中的抽象仅允许绑定单个变量，但函数术语在高级 Lean 语法中非常灵活。
syntaxFunction Abstraction
使用 Lean.Parser.Command.definition : commanddef desugar 到 Lean.Parser.Term.fun : termfun 等关键字定义的函数定义。
另一方面，归纳类型声明引入了具有函数类型（构造函数和类型构造函数）的新值，这些值本身不能仅使用 Lean.Parser.Term.fun : termfun 来实现。
syntaxCurried Functions
Lean.Parser.Term.fun : termfun 之后接受多个参数名称：
term ::= ... | fun ident ident* => term
term ::= ... | fun ident ident* : term => term
多个参数的不同类型注释需要括号：
term ::= ... | fun (ident* : term) =>term
这些相当于编写嵌套的 Lean.Parser.Term.fun : termfun 项。
在本节中描述的所有语法中，Lean.Parser.Term.fun : term=> 可以替换为 Lean.Parser.Term.fun : term↦。
函数抽象还可以使用模式匹配语法作为其参数规范的一部分，从而避免需要引入立即解构的局部变量。 有关模式匹配的部分中描述了此语法。
13.3.1. 隐式参数
Lean 支持函数的隐式参数。 这意味着 Lean 本身可以为函数提供参数，而不是要求用户提供所有需要的参数。 隐式参数分为三种：
- 普通隐式参数
普通 隐式 参数是 Lean 应通过统一确定其值的函数参数。 换句话说，每个调用站点应该恰好有一个潜在的参数值，该值将导致函数调用作为一个整体是正确类型的。 Lean精化器尝试在函数每次出现时查找所有隐式参数的值。 普通隐式参数写在花括号中（
{和}）。- 严格的隐式参数
Strictimplicit 参数与普通隐式参数相同，但 Lean 仅在调用站点提供后续显式参数时才尝试查找参数值。 严格隐式参数写在双花括号中（
⦃和⦄，或{{和}}）。- 实例隐式参数
instance隐式参数的实参可通过 类型类综合找到。 实例隐式参数写在方括号中（
[和]）。 与其他类型的隐式参数不同，不使用:编写的实例隐式参数指定参数的类型，而不是提供名称。 此外，只允许使用单个名称。 大多数实例隐式参数都会省略参数名称，因为作为函数参数合成的实例在函数体内已经可用，即使没有显式命名。
Ordinary vs Strict Implicit Parameters
syntaxFunctions with Varying Binders
Lean.Parser.Term.fun : termfun 最通用的语法接受绑定序列：
term ::= ... | fun funBinder funBinder* => term
syntaxFunction Binders
函数绑定器可以是标识符：
funBinder ::= ... | ident
带括号的标识符序列：
funBinder ::= ...
| Parentheses, used for grouping expressions (e.g., `a * (b + c)`).
Can also be used for creating simple functions when combined with `·`. Here are some examples:
- `(· + 1)` is shorthand for `fun x => x + 1`
- `(· + ·)` is shorthand for `fun x y => x + y`
- `(f · a b)` is shorthand for `fun x => f x a b`
- `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
- also applies to other parentheses-like notations such as `(·, 1)` and `(· : Nat → Nat)`
具有类型归属的标识符序列：
funBinder ::= ...
| Type ascription notation: `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
An empty type ascription `(e :)` elaborates `e` without the expected type.
This is occasionally useful when Lean's heuristics for filling arguments from the expected type
do not yield the right result.
隐式参数，带或不带类型描述：
funBinder ::= ...
| Implicit binder, like `{x y : A}` or `{x y}`.
In regular applications, whenever all parameters before it have been specified,
then a `_` placeholder is automatically inserted for this parameter.
Implicit parameters should be able to be determined from the other arguments and the return type
by unification.
In `@` explicit mode, implicit binders behave like explicit binders.
funBinder ::= ...
| Implicit binder, like `{x y : A}` or `{x y}`.
In regular applications, whenever all parameters before it have been specified,
then a `_` placeholder is automatically inserted for this parameter.
Implicit parameters should be able to be determined from the other arguments and the return type
by unification.
In `@` explicit mode, implicit binders behave like explicit binders.
instance implicits, anonymous or named:
funBinder ::= ...
| Instance-implicit binder, like `[C]` or `[inst : C]`.
In regular applications without `@` explicit mode, it is automatically inserted
and solved for by typeclass inference for the specified class `C`.
In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
funBinder ::= ...
| Instance-implicit binder, like `[C]` or `[inst : C]`.
In regular applications without `@` explicit mode, it is automatically inserted
and solved for by typeclass inference for the specified class `C`.
In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
或严格的隐式参数，带或不带类型归属：
funBinder ::= ...
| Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`.
In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert
a `_` placeholder until at least one subsequent explicit parameter is specified.
Do *not* use strict-implicit binders unless there is a subsequent explicit parameter.
Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.
Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`,
then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter,
and `h hs` has type `p y`.
In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
with `?m` a fresh metavariable.
funBinder ::= ...
| Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`.
In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert
a `_` placeholder until at least one subsequent explicit parameter is specified.
Do *not* use strict-implicit binders unless there is a subsequent explicit parameter.
Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.
Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`,
then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter,
and `h hs` has type `p y`.
In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
with `?m` a fresh metavariable.
通常，可以使用 _ 代替标识符来创建匿名参数，并且可以分别使用 {{ 和 }} 来编写 ⦃ 和 ⦄。
Lean的核心语言不区分隐式参数、实例参数和显式参数：各种函数和函数类型在定义上是相等的。 仅在精化期间才能观察到差异。
如果函数的预期类型包含隐式参数，但其绑定器不包含，则生成的函数最终可能会比代码中指示的绑定器具有更多参数。 这是因为隐式参数是自动添加的。