函数应用程序由一项、后跟一个或多个参数、或零个或多个参数以及最后的 省略号 组成。
term ::= ... | term argument+ | term argument* ..
13.4. 功能应用
通常，函数应用程序是使用并置方式编写的：参数放在函数后面，它们之间至少有一个空格。 在 Lean 的 类型论 中，所有函数都只接受一个参数并产生一个值。 所有函数应用程序都将单个函数与单个参数结合起来。 多个参数通过柯里化来表示。
高级术语语言将函数与一个或多个参数一起视为一个单元，并支持其他功能，例如隐式参数、可选参数、按名称参数以及普通位置参数。 精化器将这些转换为核心 类型论 的更简单模型。
syntaxFunction Application
syntaxArguments
函数参数可以是术语或 命名参数。
argument ::= ... | term | ((ident | _:ident) :=term)
函数的核心语言类型决定了参数在最终表达式中的位置。 函数类型包括其预期参数的名称。 在Lean的核心语言中，非依赖函数类型被编码为依赖函数类型，其中参数名称不出现在主体中。 此外，它们是内部选择的，因此它们不能写为命名参数的名称；这对于防止意外捕获很重要。
函数期望的每个参数都有一个名称。 重复函数的参数类型，从参数序列中选择参数，如下所示：
-
如果参数的名称与为命名参数提供的名称匹配，则选择该参数。
-
如果参数为 隐式，则会使用该参数的类型创建一个新的元变量并选择该元变量。
-
如果参数是 实例隐式，则使用参数的类型创建一个新的实例元变量并插入。实例元变量安排在稍后综合。
-
如果参数是 严格隐式 参数，并且存在尚未选择的任何命名或位置参数，则会使用该参数的类型创建一个新的元变量并选择该元变量。
-
如果参数是显式的，则选择并详细说明下一个位置参数。如果没有位置参数：
作为一种特殊情况，当函数应用程序出现在 pattern 中并且存在省略号时，可选参数和自动参数将变为通用模式 (_) 而不是被插入。
如果类型不是函数类型并且保留参数，则这是一个错误。
插入所有参数并有省略号后，缺失的参数将全部设置为新的元变量，就像它们是隐式参数一样。
如果为缺少显式位置参数创建了任何新变量，则整个应用程序将包装在绑定它们的 Lean.Parser.Term.fun : termfun 术语中。
最后，调用实例综合并求解尽可能多的元变量：
-
为整个函数应用程序推断类型。这可能会导致一些元变量由于类型推断期间发生的统一而被解决。
-
实例元变量被合成。仅当推断类型是作为实例之一的输出参数的元变量时，才使用 默认实例。
-
如果有预期类型，则与推断类型统一；然而，由于这种统一而产生的错误将被丢弃。如果预期类型和推断类型可以相等，则统一可以解决剩余的隐式参数元变量。如果它们不相等，则不会引发错误，因为周围的精化器可能能够插入 coercions 或 monad lifts。
Named Arguments
Lean.Parser.Command.check : command#check 命令可用于检查为函数调用插入的参数。
函数 sum3 采用三个显式 Nat 参数，名为 x、y 和 z。
def sum3 (x y z : Nat) : Nat := x + y + z
所有三个参数都可以按位置提供。
#check sum3 1 3 8
也可以按名称提供它们。
#check sum3 (x := 1) (y := 3) (z := 8)
当按名称提供参数时，可以按任何顺序。
#check sum3 (y := 3) (z := 8) (x := 1)
命名参数和位置参数可以自由混合。
#check sum3 1 (z := 8) (y := 3)
命名参数和位置参数可以自由混合。 如果参数是按名称提供的，则将使用该参数，即使它出现在可能已使用的位置参数之后。
#check sum3 1 (x := 8) (y := 3)
如果要在未提供的参数之后插入命名参数，则会创建一个函数，在其中填写所提供的参数。
#check sum3 (z := 8)
在幕后，参数的名称保存在函数类型中。 这意味着剩余的参数可以再次按名称传递。
#check (sum3 (z := 8)) (y := 1)
参数名称取自函数的type，并且函数参数使用的名称不需要与类型中使用的名称匹配。 这意味着与参数名称冲突的本地绑定不会阻止使用命名参数，因为 Lean 通过重命名函数的参数同时在类型中保持名称不变来避免这种冲突。
#check let x := 15; sum3 (z := x)
这里，命名 sum3 第一个参数的 x 已被替换，以免与周围的 Parser.Term.letlet 冲突：
即使x被重命名，它仍然可以通过名称传递：
#check (let x := 15; sum3 (z := x)) (x := 4)
这是因为该类型中仍使用名称 x。
启用选项 pp.piBinderNames 显示类型中的参数名称：
set_option pp.piBinderNames true in
#check let x := 15; sum3 (z := x)
可选参数和自动参数不是 Lean 核心 类型论 的一部分。
它们使用 optParam 和 autoParam gadgets 进行编码。
def
def
13.4.1. 广义字段表示法
关于结构字段的部分描述了从类型为结构的术语投影字段的表示法。
通用字段表示法由一个术语后跟一个点 (.) 和一个标识符组成，不以空格分隔。
syntaxField Notation
term ::= ...
| The *extended field notation* `e.f` is roughly short for `T.f e` where `T` is the type of `e`.
More precisely,
* if `e` is of a function type, `e.f` is translated to `Function.f (p := e)`
where `p` is the first explicit parameter of function type
* if `e` is of a named type `T ...` and there is a declaration `T.f` (possibly from `export`),
`e.f` is translated to `T.f (p := e)` where `p` is the first explicit parameter of type `T ...`
* otherwise, if `e` is of a structure type,
the above is repeated for every base type of the structure.
The field index notation `e.i`, where `i` is a positive number,
is short for accessing the `i`-th field (1-indexed) of `e` if it is of a structure type. 如果术语的类型是应用于零个或多个参数的常量，则 field notation 可用于向其应用函数，无论该术语是具有字段的结构还是类型类实例。 使用字段表示法来应用其他函数称为 广义字段表示法。
在术语类型的命名空间中查找点后面的标识符，这是常量的名称。
如果该类型不是常量的应用（例如元变量或 Universe），则它没有命名空间，并且不能使用通用字段表示法。
作为一种特殊情况，如果表达式是函数，则通用字段表示法将在 Function 命名空间中查找。因此，Nat.add.uncurry 是等效于 Function.uncurry Nat.add 的广义字段表示法的使用。
如果未找到该字段，但可以展开常量以产生另一种类型，即常量或常量的应用，则使用新常量重复该过程。
当找到一个函数时，点之前的项将成为该函数的参数。 具体来说，它成为第一个不会出现类型错误的显式参数。 除此之外，该应用程序像往常一样详细说明。
Generalized Field Notation
类型 Username 是常量，因此 Username 命名空间中的函数可以应用于具有通用字段表示法的 Username 类型的项。
def Username := String
其中一个函数是 Username.validate，它检查用户名是否不包含前导空格，并且仅使用一小组可接受的字符。
在其定义中，通用字段表示法用于调用函数 String.isPrefixOf、String.any、Char.isAlpha 和 Char.isDigit。
对于 String.isPrefixOf，它采用两个 String 参数，" " 用作第一个参数，因为它是点之前的项。
即使 String.any 的类型为 Username，也可以使用通用字段表示法在 name 上调用 String.any，因为未定义 Username.any 并且 Username 展开为 String。
def Username.validate (name : Username) : Except String Unit := do
if " ".isPrefixOf name then
throw "Unexpected leading whitespace"
if name.any notOk then
throw "Unexpected character"
return ()
where
notOk (c : Char) : Bool :=
!c.isAlpha &&
!c.isDigit &&
!c ∈ ['_', ' ']
def adminUser : Username := "admin"
但是，无法使用字段表示法在 "root" 上调用 Username.validate，因为 String 不会展开为 Username。
#eval "admin".validate
另一方面，adminUser 的类型为 Username，因此可以使用通用字段表示法调用 Username.validate 函数：
#eval adminUser.validate
从另一个方向来看，String.any 可以使用广义字段表示法对 Username 值 adminUser 进行调用，因为类型 Username 展开为 String。
#eval adminUser.any (· == 'm')
option
pp.fieldNotation
Default value: true
(pretty printer) use field notation when pretty printing, including for structure projections, unless '@[pp_nodot]' is applied
attributeControlling Field Notation
pp_nodot 属性导致 Lean 的漂亮打印机在打印函数时不使用字段表示法。
attr ::= ... | pp_nodot
13.4.2. 管道语法
管道语法提供了编写函数应用程序的替代方法。 重复管道使用解析优先级而不是嵌套括号来将函数应用程序嵌套到位置参数。
syntaxPipelines
右管道符号将管道右侧的术语应用于其左侧的术语。
term ::= ...
| A pipe operator that feeds values from the left into functions on the right.
`x |> f` means the same as `f x`, and it chains such that `x |> f |> g` is interpreted as `g (f x)`.
左管道符号将管道左侧的术语应用于其右侧的术语。
term ::= ...
| A pipe operator that feeds values from the right into functions on the left.
`f <| x` means the same as `f x`, except that it parses `x` with lower precedence, which means that
`f <| g <| x` is interpreted as `f (g x)` rather than `(f g) x`.
右侧管道符号背后的直觉是，左侧的值被馈送到第一个函数，其结果被馈送到第二个函数，依此类推。 在左管道表示法中，右侧的值向左馈送。
Right pipeline notation
正确的管道可用于调用一个术语上的一系列函数。 对于读者来说，他们倾向于强调正在转换的数据。
#eval "Hello!" |> String.toList |> List.reverse |> List.head!
Left pipeline notation
syntaxPipeline Fields
有一个版本的管道表示法用于 通用字段表示法。
term ::= ...
| `e |>.x` is a shorthand for `(e).x`.
It is especially useful for avoiding parentheses with repeated applications.
term ::= ...
| `e |>.x` is a shorthand for `(e).x`.
It is especially useful for avoiding parentheses with repeated applications.
e |>.f arg 是 (e).f arg 的替代语法。