# 翻译-Lean Language Reference-13-项

{{< ctxset prefix="13" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="语法" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="常量" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="选项" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="属性" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="例子" cnt_sect_lv_max="2">}}

## 13.01. 标识符 Identifiers {#S13-1}
{{< ctx level="2" >}}

{{< labelindex 
  type="语法" 
  id_alias="标识符"
>}}
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
$x:ident
```
{{< /admonition >}}

标识符项是对某个名称的引用。

> 标识符的具体词法规定
> 在 [Lean 的具体语法](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#keywords-and-identifiers) 一节中
> 有详细说明。

标识符也会出现在它们绑定名称时所处的语境，如 `let` 和 `fun`；
然而这些绑定出现处本身并不能构成完整的项。
标识符到名称的映射并不简单：
  在[模块](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#--tech-term-module)任意位置里可能有多个[命名空间](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#--tech-term-namespaces)被打开，其中
  可能有多个[小节变量](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#--tech-term-Section-variables)，也
  可能有局部绑定。
此外标识符也可能包含多个由点分隔的原子标识符；点
  既用于分隔命名空间和它们的内容，
  也用于分隔变量和字段或者是用[字段表示法](https://lean-lang.org/doc/reference/latest/Terms/Function-Application/#--tech-term-field-notation)书写的函数。
这就造成了歧义，因为标识符 `A.B.C.D.e.f` 可能指代以下任意一种情况：

- 命名空间 `A.B.C.D.e` 中的名称 `f`
  (比如 `e` 当中 `where` 块里定义的函数)。

- 常量 `A.B.C.D.e` 类型为 `T`，然后
  作为实参被塞给函数 `T.f`

- 结构常量 `A.B.C.D.e` 的字段 `f` 的投影。

- 结构常量 `A` 的一系列字段 `B`、`C`、`D`、`e` 的投影 `B.C.D.e`，
  然后再作为实参塞给函数 `f`，并用字段表示法表示函数应用。

- 如果命名空间 `Q` 被打开了，
  那么它可能是上述任何一种情况并以 `Q` 作为前缀；
  比如命名空间 `Q.A.B.C.D.e` 中的名称 `f`。

上述列表只列出了一小部分情况。
任给一个标识符，阐述器都必须查明
  该标识符究竟指代哪（几）个名称、
  尾部的内容究竟是字段还是以字段表示法描述的函数应用。
这就是名称的**解析 Resolving**。

某些全局环境中的声明在第一次被引用时会被惰性创建。
如果在解析 Resolving 标识符的过程中
  既创建了这样的声明，
  又产生了对它的引用，
那么该解析就可被称作名称的**实现 Realizing**。
名称解析和实现的规则是相同的，因此
尽管本小节仅提及名称解析 Resolving ，
但它也同样适用于名称实现 Realizing 。

名称解析受下述因素影响：

- [预解析 Pre-Resolved 名称](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Macros/#--tech-term-pre-resolved-identifiers)
  被附加到标识符上。

- [宏作用域](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Macros/#--tech-term-macro-scopes)
  被附加到标识符上。

- 作用域内的局部绑定。
  作为 `let rec` 阐述的一部分被创建的辅助定义也囊括在内。

- 位于被当前模块传递导入的模块当中，
  由 [`export`](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#Lean___Parser___Command___export) 创建的别名。

- 当前[小节作用域](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#--tech-term-section-scope)，尤其是
  当前[命名空间](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#--tech-term-current-namespace)、
  已打开的命名空间、
  小节变量。

标识符的任何前缀都可以被解析为一组名称。
那些没被包含在解析过程中的后缀
随后会被当作字段投影或字段表示法处理。
较长的前缀解析优先级高于
较短的前缀；也就是说，
标识符中被当作字段表示法处理的部分会尽可能地少。
标识符前缀可能是以下列表中的任何一项，
列表当中上方条目的优先级高于下方条目：

1.  一个局部受缚变量，其名称完全等同于标识符前缀（包括宏作用域），
    其中内层局部绑定的优先级高于外层局部绑定。

    A locally-bound variable whose name is 
    identical to the identifier prefix, 
    including macro scopes, with 
    closer local bindings taking precedence over 
    outer local bindings.

2.  一个局部辅助定义，
    其名称完全等同于标识符前缀。

    A local auxiliary definition
    whose name is identical to the identifier prefix

3.  一个[小节变量](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#--tech-term-Section-variables)，
    其名称完全等同于标识符前缀。
  
    A [section variable](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#--tech-term-Section-variables)
    whose name is identical to the identifier prefix

4.  一个全局名称，要么
    其名称等同于将当前命名空间前缀附加到标识符前缀上，要么
    [当前命名空间](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#--tech-term-current-namespace)的某个前缀里存在与之对应的别名。
    当前命名空间较长的前缀优先级高于较短的前缀。

    A global name 
      that is identical to a prefix of the current namespace appended to the identifier prefix, or 
      for which an alias exists in a prefix of the [current namespace](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#--tech-term-current-namespace), 
    with longer prefixes of the current namespace taking precedence over 
    shorter ones

5.  一个全局名称，
    其名称完全等同于标识符前缀，且
    其通过 `open` 命令引入作用域。
    
    A global name that has been brought into scope 
    via [`open`](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#Lean___Parser___Command___open) commands that is identical to the identifier prefix

如果标识符被解析为多个名称，
那么阐述器就会尝试使用所有名称。
如果恰好有一个成功，
那么它就会被用作该标识符的含义。
如果有多个成功或者全部失败，
那么就会报错。

If an identifier resolves to multiple names, 
then the elaborator attempts to use all of them. 
If exactly one of them succeeds, 
then it is used as the meaning of the identifier. 
It is an error if more than one succeed or if all fail.

{{< labelindex 
  type="例子" 
  summary="局部名称优先"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：局部名称优先" 
  open=false
>}}
局部绑定优先级高于全局绑定：

```lean {wrapper=false, lineNos=false}
def x := "global"
#eval
  let x := "local"
  x
-- "local"
```

最内层的局部绑定优先级高于其他绑定：

```lean {wrapper=false, lineNos=false}
#eval
  let x := "outer"
  let x := "inner"
  x
-- "inner"
```
{{< /admonition >}}


{{< labelindex 
  type="例子" 
  summary="当前命名空间内前缀更长的优先"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：当前命名空间内前缀更长的优先" 
  open=false
>}}
命名空间 `A`、`B`、`C` 一层套一层。
命名空间 `A`、`C` 都包含一个 `x` 的声明：

```lean {wrapper=false, lineNos=false}
namespace A
def x := "A.x"
namespace B
namespace C
def x := "A.B.C.x"
```

如果当前命名空间是 `A.B.C`，
那么 `x` 会被解析为 `A.B.C.x`。

```lean {wrapper=false, lineNos=false}
#eval x
-- "A.B.C.x"
```

如果当前命名空间是 `A.B`，
那么 `x` 会被解析为 `A.x`。

```lean {wrapper=false, lineNos=false}
end C
#eval x
-- "A.x"
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="标识符前缀更长的优先"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：标识符前缀更长的优先" 
  open=false
>}}
当标识符可能指代不同的来自名称的投影时，
前缀更长的那个优先级更高：

```lean {wrapper=false, lineNos=false}
structure A where
  y : String
deriving Repr

structure B where
  y : A
deriving Repr

def y : B := ⟨⟨"shorter"⟩⟩
def y.y : A := ⟨"longer"⟩
```

给定上述声明，`y.y.y` 照理来说既可能
  指代的是 `y` 的 `y` 字段的 `y` 字段，也可能
  指代的是 `y.y` 的 `y` 字段；然而
其指的却是 `y.y` 的 `y` 字段，
因为在所有 `y.y.y` 的前缀中 `y.y` 是更长的那个：

```lean {wrapper=false, lineNos=false}
#eval y.y.y
-- "longer"
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="当前命名空间优先级高于已开启的命名空间"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：当前命名空间优先级高于已开启的命名空间"
  open=false 
>}}
如果一个标识符指代的可能是
   一个当前命名空间的前缀中定义的名称，或者是
  一个已打开的命名空间中的名称，
那么前者优先级更高。

```lean {wrapper=false, lineNos=false}
namespace A
def x := "A.x"
end A

namespace B
def x := "B.x"
namespace C
open A
#eval x
```

即便命名空间 `A` 的开启比常量 `B.x` 的声明更近，
标识符 `x` 仍然会被解析为 `B.x` 而不是 `A.x`；
这是因为 `B` 是当前命名空间 `B.C` 的前缀。

```lean {wrapper=false, lineNos=false}
#eval x
-- "B.x"
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="标识符有歧义"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：标识符有歧义" 
  open=false
>}}
在本例中，`x` 既可能
  指代 `A.x`，也可能
  指代 `B.x`，
然而两者都没有优先级，
这是因为两者类型相同。
所以产生报错。

```lean {wrapper=false, lineNos=false}
def A.x := "A.x"
def B.x := "B.x"
open A
open B
#eval x
-- Ambiguous term
--   x
-- Possible interpretations:
--   B.x : String  
--   A.x : String
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="类型注解消除歧义"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类型注解消除歧义" 
  open=false
>}}
如果原本会产生歧义的名称拥有不同的类型，
那么系统会利用类型来消除歧义：

```lean {wrapper=false, lineNos=false}
def C.x := "C.x"
def D.x := 3
open C
open D
#eval (x : String)
-- "C.x"
```
{{< /admonition >}}

### 13.01.01. 前缀 `.` Leading `.` {#S13-1-1}
{{< ctx level="3" >}}

==TODO==

## 13.02. 函数类型构造 Function Types {#S13-2}
{{< ctx level="2" >}}

Lean 的函数类型描述的不仅仅只有函数的定义域和陪域，
它们为函数应用位置的阐述提供了指导：
  一部分形参应通过
    合一或者是
    [类型类合成](https://lean-lang.org/doc/reference/latest/Type-Classes/Instance-Synthesis/#instance-synth)来自动发现，
  另外一部分形参为带默认值的可选参数，
  剩下的形参则应该通过自定义的策略脚本来合成。
此外它们的语法还支持[柯里化函数](https://lean-lang.org/doc/reference/latest/The-Type-System/Functions/#--tech-term-currying)的缩写。

{{< labelindex 
  type="语法" 
  id_alias="单参函数类型构造"
>}}
`(… : …) → …`\
`… → …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
依值函数类型包含一个显式名称：

```lean {wrapper=false, lineNos=false}
term ::= ...
  | (ident : term) → term
```

非依值函数类型则没有：

```lean {wrapper=false, lineNos=false}
term ::= ...
  | term → term
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="多参函数类型构造"
>}}
`(… : …) → …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
依值函数类型可能包含多个形参，
它们具有相同的类型，并且被包裹在一对圆括号内：

```lean {wrapper=false, lineNos=false}
term ::= ...
  | (ident* : term) → term
```

这等同于在嵌套的函数类型中
重复为每个形参补充类型注解。
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="函数类型构造（隐式、可选、自动形参声明）"
>}}
`(… : … := …) → …`\
`(… : … := by …) → …`\
`{… : …} → …`\
`[…] → …`\
`[… : …] → …`\
`⦃… : …⦄ → …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
函数类型可以描述那些类型中带有隐式、可选和自动形参的函数。
除实例隐式形参外的其余形参都需要一或多个名称。

```lean {wrapper=false, lineNos=false}
term ::= ...
  | (ident* : term := term) → term
term ::= ...
  | (ident* : term := by tacticSeq) → term
term ::= ...
  | {ident* : term} → term
term ::= ...
  | [term] → term
term ::= ...
  | [ident : term] → term
term ::= ...
  | ⦃ident* : term⦄ → term
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="函数类型构造（多个同类型形参声明）"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：函数类型构造（多个同类型形参声明）" 
  open=false
>}}
[`Nat.add`](https://lean-lang.org/doc/reference/latest/Basic-Types/Natural-Numbers/#Nat___add) 的类型可以写成下述形式：

- `Nat → Nat → Nat`

- `(a : Nat) → (b : Nat) → Nat`

- `(a b : Nat) → Nat`

三个写法都是等价的，只不过最后两种写法
允许函数实参以[具名实参](https://lean-lang.org/doc/reference/latest/Terms/Function-Application/#--tech-term-named-arguments)的形式表示。
{{< /admonition >}}

## 13.03. 函数构造 Functions {#S13-3}
{{< ctx level="2" >}}

函数类型下的项可以通过函数抽象构造，
这是通过 `fun` 关键字引入的。

> 函数抽象在其他社群中也被称作 *lambda*，
>   源于 Alonzo Church 为其创建的记号；
> 又或者被称作是匿名函数，
>   因为它们不需要在全局环境中被命名。

尽管函数抽象在 Lean 的核心类型理论中只允许绑定单个形参，
但是在高层次的 Lean 语法中函数项的写法却相当灵活。

{{< labelindex 
  type="语法" 
  id_alias="单参函数抽象"
>}}
`fun … => …`\
`fun … : … => …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
最基础的函数抽象会
  引入一个变量来
  表示函数的形参：

```lean {wrapper=false, lineNos=false}
term ::= ...
  | fun ident => term
```

Lean 在阐述代码的时候必须能够确定函数的定义域，
一种提供信息的方式是类型注解：

```lean {wrapper=false, lineNos=false}
term ::= ...
  | fun ident : term => term
```
{{< /admonition >}}

通过 `def` 声明的函数常量最后都会被脱糖变成 `fun` 的形式。另一方面，
归纳类型声明会引入函数类型下新的值（构造器、类型构造器），
而这些值本身无法仅通过 `fun` 来构造。

{{< labelindex 
  type="语法" 
  id_alias="多参函数抽象"
>}}
`fun … => …`\
`fun … : … => …`\
`fun (… : …) => …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
`fun` 后面声明多个形参也是允许的：

```lean {wrapper=false, lineNos=false}
term ::= ...
  | fun ident ident* => term
term ::= ...
  | fun ident ident* : term => term
```

多个形参的类型注解补充需要用上圆括号：

```lean {wrapper=false, lineNos=false}
term ::= ...
  | fun (ident* : term) =>term
```

上述语法等价于嵌套的 `fun` 项。
{{< /admonition >}}

本小节中提到的 `=>` 都可以替换为 `↦`。

函数抽象也可以通过模式匹配语法来声明形参，
如此便不必再引入一个局部变量然后再将其解构。
在[模式匹配相关的小节](https://lean-lang.org/doc/reference/latest/Terms/Pattern-Matching/#pattern-fun)中有详细介绍。

### 13.03.01. 隐式形参 Implicit Parameters {#S13-3-1}
{{< ctx level="3" >}}

Lean 允许函数使用隐式形参，意味着
Lean 自己就可以为函数提供实参，用户不需要为其操心。
隐式形参有以下三种类别：

- **普通隐式形参 Ordinary Implicit Parameters**

  普通隐式形参需要 Lean 通过合一来确定对应实参的值。换句话说，
  函数的所有被调用处都应该有一个潜在的实参值与之对应，
  使得完整的函数调用是良类型 Well-Typed 的。Lean 的阐述器会尽可能地
  为函数的每个隐式形参的各个出现找到对应的值。
  普通隐式形参声明用花括号（`{` 和 `}`）包裹。

- **严格隐式形参 Strict Implicit Parameters**

  严格隐式形参与普通隐式形参完全相同，唯一的区别是
  只有在函数被调用处提供了后续的显式实参时
  Lean 才会尝试去寻找（该严格隐式形参）对应实参的值。
  严格隐式形参写在双花括号（`⦃` 和 `⦄`，或 `{{` 和 `}}`）中。

- **实例隐式形参 Instance Implicit Parameters**

  实例隐式形参的实参是通过类型类合成来寻找的。
  实例隐式形参写在方括号（`[` 和 `]`）中。
  与其他类型的隐式形参不同，
  不带 `:` 的实例隐式形参会
    指定该形参的类型，而不是
    提供一个形参名。
  此外只允许指定单个名称。
  大多数实例隐式形参都会直接省略形参名称，
  因为被合成为函数形参的实例
  即使没有被显式命名
  在函数体内也已经是直接可用的。

  Arguments for instance implicit parameters are found via type class synthesis. 
  Instance implicit parameters are written in square brackets (`[` and `]`). 
  Unlike the other kinds of implicit parameter, 
  instance implicit parameters that are written without a `:` 
    specify the parameter's type rather than 
    providing a name. 
  Furthermore, only a single name is allowed. 
  Most instance implicit parameters omit the parameter name because 
  instances synthesized as parameters to functions are already available 
  in the functions' bodies, even without being named explicitly.

{{< labelindex 
  type="例子" 
  summary="函数抽象（普通、严格隐式类型形参声明）"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：函数抽象（普通、严格隐式形参声明）" 
  open=false
>}}
函数 `f` 与 `g` 之间的差别在于
`α` 在 `g` 中是严格隐式的：

```lean {wrapper=false, lineNos=false}
def f {α : Type} : α → α := fun x => x
def g ⦃α : Type⦄ : α → α := fun x => x
```

在被应用于具体实参时，
这些函数的阐述过程是完全相同的：

```lean {wrapper=false, lineNos=false}
example : f 2 = g 2 := rfl
```

使用 `f` 需要求解隐式的 `α`，
缺乏足够可用的信息会导致阐述失败：

```lean {wrapper=false, lineNos=false}
example := f
-- don't know how to synthesize implicit argument `α`
--   @f ?m.3
-- context:
-- ⊢ Type
```

然而未提供显式实参时，
使用 `g` 并不需要求解隐式的 `α`：

```lean {wrapper=false, lineNos=false}
example := g
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="函数抽象"
>}}
`fun … => …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
更宽泛的 `fun` 语法允许接收一连串的绑定器 `funBinder`：

```lean {wrapper=false, lineNos=false}
term ::= ...
  | fun funBinder funBinder* => term
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="形参声明（显式、隐式类型注解省略、补充）"
>}}
`([anonymous]…)`\
`([anonymous]… : …)`\
`{…}`\
`{… : …}`\
`[…]`\
`[… : …]`
`⦃…⦄`\
`⦃… : …⦄`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
函数绑定器可以只是标识符：

```lean {wrapper=false, lineNos=false}
funBinder ::= ...
  | ident
```

也可以是一连串标识符序列，包裹在圆括号内：

```lean {wrapper=false, lineNos=false}
funBinder ::= ...
  | ([anonymous]ident ident*)
```

也可以是一连串标识符序列，后面跟着一个类型注解，然后一起包裹在圆括号内：

```lean {wrapper=false, lineNos=false}
funBinder ::= ...
  | ([anonymous]ident ident* : term)
```

普通隐式形参，类型注解存在与否的情况：

```lean {wrapper=false, lineNos=false}
funBinder ::= ...
  | {ident ident*}
funBinder ::= ...
  | {ident ident* : term}
```

严格隐式形参，类型注解存在与否的情况

```lean {wrapper=false, lineNos=false}
funBinder ::= ...
  | ⦃ident ident*⦄
funBinder ::= ...
  | ⦃ident* : term⦄
```

实例隐式形参，匿名或具名的情况：

```lean {wrapper=false, lineNos=false}
funBinder ::= ...
  | [term]
funBinder ::= ...
  | [ident : term]
```

和前面类似，
  `_` 可以代替标识符来创建匿名形参，
  `⦃` 和 `⦄` 可以分别用 `{{` 和 `}}` 代替。
{{< /admonition >}}

Lean 的核心语言
并不区分普通隐式、实例隐式和显式形参：
各种不同的函数和函数类型在底层都是定义等价 Definitional Equal 的。
这种区别只有在阐述的过程中才能被观察到。

如果一个函数的预期类型包含了隐式形参，
但是函数绑定器中却没有显示地写出这些隐式形参，
那么最终生成的函数带有的形参数量可能会多于
  代码绑定器中体现出的数量。
因为隐式形参会被自动添加进去。

{{< labelindex 
  type="例子" 
  summary="函数抽象（隐式类型形参声明）"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：函数抽象（隐式类型形参声明）" 
  open=false
>}}
恒等函数可以声明为只有单个显式形参的形式。
只要知道了实参的类型，隐式形参就会被自动添加进去。

```lean {wrapper=false, lineNos=false}
#check (fun x => x : {α : Type} → α → α)
-- fun {α} x => x : {α : Type} → α → α
```

下述代码都是等价的：

```lean {wrapper=false, lineNos=false}
#check (fun {α} x => x : {α : Type} → α → α)
-- fun {α} x => x : {α : Type} → α → α
#check (fun {α} (x : α) => x : {α : Type} → α → α)
-- fun {α} x => x : {α : Type} → α → α
#check (fun {α : Type} (x : α) => x : {α : Type} → α → α)
-- fun {α} x => x : {α : Type} → α → α
```
{{< /admonition >}}

## 13.04. 函数应用 Function Application {#S13-4}
{{< ctx level="2" >}}

通常情况下，函数应用是通过并列的方式来书写的：
实参置于函数之后，两者之间至少存在一个空格。
在 Lean 的类型理论中，所有函数都
  接收一个实参并
  产生一个唯一与之对应的值。
所有函数应用本质上都是单个函数与
  单个实参的组合。
  多个实参的情况则通过柯里化来表示。

面向用户的高层次项语言
  会将函数与一个或多个实参视为一个统一的整体，并且还
  支持如
    隐式实参、
    可选实参、
    具名实参等附加功能，外加普通的
    位置实参
阐述器会将这些东西转换为核心类型理论里更为简单的模型。

{{< labelindex 
  type="语法" 
  id_alias="函数应用"
>}}
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
函数应用包含一个项，其后
  可以跟着一个或多个实参，
  或是跟着零个或多个实参外加一个省略号。

```lean {wrapper=false, lineNos=false}
term ::= ...
  | term argument+
  | term argument* ..
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="位置、具名实参构造"
>}}
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
实参要么是
  项，要么就是
  具名实参。

```lean {wrapper=false, lineNos=false}
argument ::= ...
  | term
  | ((ident | _:ident) :=term)
```
{{< /admonition >}}

函数在核心语言中的类型决定了实参在最终表达式里的位置。
函数类型里包含了它们所期待的形参的名称。在 Lean 的核心语言中，
  非依值函数类型也会被编码为依值函数类型，只不过对于后者
    形参名称不会出现在函数体中==TODO==；此外
    它们在内部会被选中，使其无法被写成具名实参的名称，
  这对预防意外捕获至关重要。

函数期待每个形参都有一个名称。
通过遍历函数实参的种类，
Lean 会从实参列表中选中实参。方式如下：

- 如果形参名称与具名实参的名称匹配，
  那么该实参将被选中。

- 如果形参是[普通隐式的](https://lean-lang.org/doc/reference/latest/Terms/Functions/#--tech-term-implicit)，
  那么一个新的元变量将被创建并被选中，元变量类型为该形参的类型。

- 如果形参是[实例隐式的](https://lean-lang.org/doc/reference/latest/Type-Classes/#--tech-term-instance-implicit)，
  那么一个新的元变量将被创建并被插入，元变量类型为该形参的类型。
  实例元变量将被用于稍后进行的合成。

- 如果形参是[严格隐式的](https://lean-lang.org/doc/reference/latest/Terms/Functions/#--tech-term-Strict-implicit)
  并且还存在任何未被选中的具名实参或位置实参，
  那么一个新的元变量将被创建并被选中，元变量类型为该形参的类型。

- 如果形参是显式的，
  那么接下来的位置实参将被选中并被阐述。
  如果没有位置实参的话：

  - 如果形参为[可选的](https://lean-lang.org/doc/reference/latest/Definitions/Headers-and-Signatures/#--tech-term-optional-parameters)，
    那么其默认值将作为实参被选中。

  - 如果形参为[自动的](https://lean-lang.org/doc/reference/latest/Definitions/Headers-and-Signatures/#--tech-term-automatic-parameters)，
    那么与之关联的策略脚本将被执行以构造实参。

  - 如果形参既不是可选的又不是自动的，
    并且
    
    - 如果省略号没有，
      那么一个新的变量将作为实参被选中。
    
    - 如果省略号存在，
      那么一个新的元变量将被选中，同隐式形参的情形。

作为一个特殊情况，当
  函数应用出现在[模式](https://lean-lang.org/doc/reference/latest/Terms/Pattern-Matching/#pattern-matching)当中，并且
  省略号存在时，
可选实参和自动实参
  不会被插入，
  而是会变成通用模式（`_`）。

As a special case, when 
  the function application occurs in a [pattern](https://lean-lang.org/doc/reference/latest/Terms/Pattern-Matching/#pattern-matching) and 
  there is an ellipsis, 
optional and automatic arguments become universal patterns (`_`) 
instead of being inserted.

如果类型不是函数类型并且还有剩余实参，
那么会有报错。
如果所有实参都被插入完后还存在省略号，
那么缺失的实参就会被统统设置为新的元变量，
就好像这些实参是隐式的一样。
如果新变量是为了缺失的显式位置实参而创建的，
那么整个函数应用表达式就会被包裹在一个 `fun` 表达式中来绑定这些变量。
最后，实例合成会被启用，
元变量会被尽可能多地求解：

It is an error if the type is not a function type and arguments remain. 
After all arguments have been inserted and there is an ellipsis, 
then the missing arguments are all set to fresh metavariables, 
just as if they were implicit arguments. 
If any fresh variables were created for missing explicit positional arguments, 
the entire application is wrapped in a `fun` term that binds them. 
Finally, instance synthesis is invoked and 
as many metavariables as possible are solved:

1.  完整函数应用表达式的类型会被推断。
    这可能导致一些元变量被求解，
    因为类型推断过程中会发生合一。

    A type is inferred for the entire function application. 
    This may cause some metavariables to be solved 
    due to unification that occurs during type inference.

2.  实例元变量会被合成。
    只有在
      被推断出的类型是个元变量，并且
      该元变量是某个实例输出的参数时，
    [默认实例](https://lean-lang.org/doc/reference/latest/Type-Classes/Instance-Synthesis/#--tech-term-default-instances)才会被使用。

    The instance metavariables are synthesized. 
    [Default instances](https://lean-lang.org/doc/reference/latest/Type-Classes/Instance-Synthesis/#--tech-term-default-instances) are only used if the inferred type is a metavariable 
    that is the output parameter of one of the instances.

3.  如果存在预期类型，
    那么它会与被推断出的类型进行合一；
    然而由此合一所产生的错误会被丢弃。
    如果预期类型和被推断出的类型可以相等，
    那么合一可以解决剩余的隐式实参元变量。
    如果它们不相等，则不会抛出错误，
    因为周围的阐述器可能能够插入[类型强制转换](https://lean-lang.org/doc/reference/latest/Coercions/#--tech-term-coercion)或[单子提升](https://lean-lang.org/doc/reference/latest/Functors___-Monads-and--do--Notation/Syntax/#Lean___Parser___Term___do)。

    If there is an expected type, it is unified with the inferred type; however, 
    errors resulting from this unification are discarded. 
    If the expected and inferred types can be equal, 
    unification can solve leftover implicit argument metavariables. 
    If they can't be equal, an error is not thrown 
    because a surrounding elaborator may be able to insert [coercions](https://lean-lang.org/doc/reference/latest/Coercions/#--tech-term-coercion) or [monad lifts](https://lean-lang.org/doc/reference/latest/Functors___-Monads-and--do--Notation/Syntax/#Lean___Parser___Term___do).

{{< labelindex 
  type="例子" 
  summary="位置、具名实参构造"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：位置、具名实参构造" 
  open=false
>}}
[`#check`](https://lean-lang.org/doc/reference/latest/Interacting-with-Lean/#Lean___Parser___Command___check) 命令
可以用来检查函数应用时所插入的实参。

函数 `sum3`
  有三个类型为 `Nat` 的显式形参，
  分别名为 `x`、`y` 和 `z`。

```lean {wrapper=false, lineNos=false}
def sum3 (x y z : Nat) : Nat := x + y + z
```

三个实参可以被写成位置实参的形式：

```lean {wrapper=false, lineNos=false}
#check sum3 4 3 8
-- sum3 4 3 8 : Nat
```

也可以写成具名实参的形式：

```lean {wrapper=false, lineNos=false}
#check sum3 (x := 4) (y := 3) (z := 8)
-- sum3 4 3 8 : Nat
```

当实参被写成具名实参形式时，
它们的排列顺序可以是任意的。

```lean {wrapper=false, lineNos=false}
#check sum3 (y := 3) (x := 4) (z := 8)
-- sum3 4 3 8 : Nat
```

具名实参和位置实参可随意混合使用。

```lean {wrapper=false, lineNos=false}
#check sum3 (y := 3) 8 (x := 4)
-- sum3 4 3 8 : Nat
```

具名实参和位置实参可随意混合使用。
如果某个实参被写成了具名实参的形式，
那么即便它前面是一个可能被使用了的位置实参，
它也仍然会被选作实参。

```lean {wrapper=false, lineNos=false}
#check sum3 8 (y := 3) (x := 4) 
-- sum3 4 3 8 : Nat
```

如果将具名实参插入到未被提供的位置实参后面，
那么一个函数将会被创建，当中已提供的实参将会被填充。

```lean {wrapper=false, lineNos=false}
#check sum3 (y := 3)
-- fun x ↦ sum3 x 3 : Nat → Nat → Nat
-- fun x ↦ sum3 x 3 : (x z : Nat) → Nat
```

形参的名称在背后其实会被保存在函数类型中，
这意味着剩余的实参也可以再次被写成具名实参的形式：

```lean {wrapper=false, lineNos=false}
#check (sum3 (y := 3)) (x := 4)
-- (fun x ↦ sum3 x 3) 4 : Nat → Nat
-- (fun x ↦ sum3 x 3) 4 : (z : Nat) → Nat
```

尽管形参名称往往取自函数类型，
但是形参名称不必非得等同于函数类型中所使用的名称。
这意味着即便局部声明与形参名称发生冲突，也不会影响具名实参的使用；
因为形参名称在这里会被临时修改以避免冲突。函数类型中则仍保持不变。

在下面的例子中，原先被拿来命名 `sum3` 首个形参的 `x`
已经被重命名了，以避免与 `let` 里面的 `x` 发生冲突：

```lean {wrapper=false, lineNos=false}
#check let x := 8 ; sum3 (z := x)
-- let x := 8;
-- fun x_1 y ↦ sum3 x_1 y x : Nat → Nat
-- fun x_1 y ↦ sum3 x_1 y x : (x y : Nat) → Nat
```

即便 `x` 被重命名为 `x_1`，
其仍然可以被用在具名实参中：

```lean {wrapper=false, lineNos=false}
#check (let x := 8 ; sum3 (z := x)) (x := 4)
-- (let x := 8;
--  fun x_1 y ↦ sum3 x_1 y x) 4
-- : Nat → Nat
-- : (y : Nat) → Nat
```

这是因为名称 `x` 依然被用于函数类型中。
启用选项 `pp.piBinderNames` 
可以显示函数类型中形参的名称：

```lean {wrapper=false, lineNos=false}
set_option pp.piBinderNames true in
#check let x := 8 ; sum3 (z := x)
-- let x := 8;
-- fun x_1 y ↦ sum3 x_1 y x : Nat → Nat
-- fun x_1 y ↦ sum3 x_1 y x : (x y : Nat) → Nat
```
{{< /admonition >}}

可选形参和自动形参
都不是 Lean 核心类型理论内的概念。
它们分别是通过以下两个[零件 Gadget](https://lean-lang.org/doc/reference/latest/Type-Classes/Class-Declarations/#--tech-term-gadgets) 实现的：
[`optParam`](https://lean-lang.org/doc/reference/latest/Terms/Function-Application/#optParam) 和
[`autoParam`](https://lean-lang.org/doc/reference/latest/Terms/Function-Application/#autoParam) ==TODO==。

{{< labelindex 
  type="常量" 
  id_alias="optParam"
>}}
零件 Gadget，用于实现可选形参
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
optParam.{u} (α : Sort u) (default : α) : Sort u
```

一个零件 Gadget，用于实现可选形参。

A binder like `(x : α := default)` in a declaration 
  is syntax sugar for `x : optParam α default`, and 
  triggers the elaborator to attempt to use `default` to 
    supply the argument if it is not supplied.
{{< /admonition >}}

{{< labelindex 
  type="常量" 
  id_alias="autoParam"
>}}
零件 Gadget，用于实现自动形参
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u
```

一个零件 Gadget，用于实现自动形参。

This is similar to the [`optParam`](#常量-optParam) gadget, 
but it uses the given tactic. Like [`optParam`](#常量-optParam), this gadget 
only affects elaboration. For example, 
the tactic will *not* be invoked during type class resolution.
{{< /admonition >}}

### 13.04.01. 广义字段表示法 Generalized Field Notation {#S13-4-1}
{{< ctx level="3" >}}

[结构字段相关的小节](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#structure-fields)
里介绍了一种表示法，如此便可以类似投影的方式
获取类型为结构的项的各个字段。
广义字段表示法通常是一个项后面
跟着一个点（`.`）以及一个标识符。
三者之间没有空格。

{{< labelindex 
  type="语法" 
  id_alias="函数应用（广义字段表示法）"
>}}
`… . …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
term ::= ...
  | term.ident
```
{{< /admonition >}}

如果一个项的类型形如某个常量被应用于零个或多个实参上，
那么字段表示法就也可被拿来表示某个函数在该项上的应用，
无论该项是结构实例还是类型类实例（它们都拥有字段）。
使用字段表示法来应用其他函数的写法被称为
**广义字段表示法 Generalized Field Notation**。

点后面的标识符会在项类型对应的命名空间中进行查找，
命名空间的名称即类型常量的名称。
如果类型并不是形如某个常量的应用（如元变量或宇宙），
那么它就没有命名空间，广义字段表示法也就无法使用。
作为一种特殊情况，如果一个表达式是函数，
那么广义字段表示法就会在 `Function` 命名空间中进行查找；
如此 `Nat.add.uncurry` 其实就相当于
`Function.uncurry Nat.add`。

如果字段没有被找到
但是常量可以被展开 unfold 并产生一个类型，
那么这套操作过程就会再继续针对新类型执行。

当一个函数被读取到时，
点前面的项会变成函数的一个实参。具体点说，
它会变成函数的首个类型匹配成功的显式实参。
此后函数应用的阐述过程就和普通情况一样了。

{{< labelindex 
  type="例子" 
  summary="函数应用（广义字段表示法）"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：函数应用（广义字段表示法）" 
  open=false
>}}
类型 `Username` 是一个常量，
因此 `Username` 命名空间中的函数
应用于 `Username` 下的项的过程
就可以通过广义字段表示法来表示

```lean {wrapper=false, lineNos=false}
def Username := String
```

我们可以拿 `Username.validate` 来做示范：
其用于检查
  用户名的头部是否为空格，以及
  用户名是否只用到允许使用的一小部分字符。
在其定义中，广义字段表示法
被用来调用函数
  `String.isPrefixOf`、
  `String.any`、
  `Char.isAlpha` 和
  `Char.isDigit`。
`String.isPrefixOf` 接收两个类型为 `String` 的实参，
  `" "` 被选为第一个实参，因为它是点前面的项。
`String.any` 在 `name` 上的应用可以通过广义字段表示法来表示，
  即便 `name` 的类型为 `Username`；
  因为 `Username.any` 并没有被定义，
  并且 `Username` 会被展开 unfold 为 `String`。

```lean {wrapper=false, lineNos=false}
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"
```

但是 `Username.validate` 在 `"root"` 上的应用
不能通过广义字段表示法来表示，
因为 `String` 无法被展开 unfold 为 `Username`。

```lean {wrapper=false, lineNos=false}
#eval "admin".validate
-- Invalid field `validate`: The environment does not contain 
-- `String.validate`, so it is not possible to 
-- project the field `validate` from an expression
--   "admin"
-- of type `String`
```

另一方面，`adminUser` 的类型是 `Username`，
因此 `Username.validate` 函数
就可以通过广义字段表示法来应用：

```lean {wrapper=false, lineNos=false}
#eval adminUser.validate
-- Except.ok ()
```

反过来，`String.any` 在
`adminUser : Username` 上的应用
就可以通过广义字段表示法来表示：

```lean {wrapper=false, lineNos=false}
#eval adminUser.any (· == 'm')
-- true
```
{{< /admonition >}}

{{< labelindex 
  type="选项" 
  id_alias="pp.fieldNotation"
  summary="默认为 `true`"
>}}
美观打印时会使用字段表示法，除非 `@[pp_nodot]` 被应用
{{< /labelindex >}}
{{< admonition 
  type=info
  title="选项：`{{< indexprint >}}`" 
>}}
默认值：[`true`](https://lean-lang.org/doc/reference/latest/Basic-Types/Booleans/#Bool___false)

（美观打印器）在美观打印的时候
会使用字段表示法（结构投影也会），
除非 `@[pp_nodot]` 被应用。
{{< /admonition >}}

{{< labelindex 
  type="属性" 
  id_alias="pp_nodot"
>}}
字段表示法启用 / 禁用
{{< /labelindex >}}
{{< admonition 
  type=info
  title="属性：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
attr ::= ...
  | pp_nodot
```

`pp_nodot` 属性可以让 Lean 的美观打印器
在打印函数的时候不使用字段表示法。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="函数应用的类型打印（字段表示法启用、禁用）"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：函数应用的类型打印（字段表示法启用、禁用）" 
  open=false
>}}
`Nat.half` 默认以字段表示法打印：

```lean {wrapper=false, lineNos=false}
def Nat.half : Nat → Nat
  | 0 | 1 => 0
  | n + 2 => n.half + 1
#check Nat.half Nat.zero
-- Nat.zero.half : Nat
```

将 `pp_nodot` 添加在 `Nat.half` 上
会导致项以普通函数应用语法显示。

```lean {wrapper=false, lineNos=false}
attribute [pp_nodot] Nat.half
#check Nat.half Nat.zero
-- Nat.half Nat.zero : Nat
```
{{< /admonition >}}

### 13.04.02. 管道语法 Pipeline Syntax {#S13-4-2}
{{< ctx level="3" >}}

## 13.10. 类型注解 Type Ascriptions {#S13-10}
{{< ctx level="2" >}}

类型注解显式地为项添加类型信息，
它们是为 Lean 指明项的预期类型的一种方式。
被注解的这个类型必须定义等价 Definitional Equal 于
Lean 基于项所处语境所推断出的类型。
类型注解不仅仅用于记录程序：

- 程序文本可能没有足够的信息用于推断项的类型。
  类型注解是提供类型信息的一种方式。

- 项被推断出的类型可能与用户预期类型不符
  程序文本可能包含足够的信息用于推导项的类型，
  但推导出的类型可能不是用户所期待的。

- 项的预期类型会驱动 Lean 插入[类型强制转换](https://lean-lang.org/doc/reference/latest/Coercions/#--tech-term-coercion)，
  而类型注解是控制强制转换插入位置的一种方式。

{{< labelindex 
  type="语法" 
  id_alias="类型后缀注解"
>}}
`([anonymous]… : …)`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
类型注解必须置于圆括号当中。
它们指示第一个项的类型是第二个项。

```lean {wrapper=false, lineNos=false}
term ::= ...
  | ([anonymous]term : term)
```
{{< /admonition >}}

某些地方需要的类型注解可能会很冗长，比如策略证明或者是 [`do` 代码块](https://lean-lang.org/doc/reference/latest/Functors___-Monads-and--do--Notation/Syntax/#Lean___Parser___Term___do)。
  在上述情况中类型后缀注解可能会难以阅读，因为必须用到圆括号；此外
  项的类型对于理解证明和 `do` 代码块是至关重要的。
在这些情况下，前缀版本的类型注解可能更易于阅读。

{{< labelindex 
  type="语法" 
  id_alias="类型前缀注解"
>}}
`show … from …`\
`show … by …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
term ::= ...
  | show term from term
```

当 `show` 表达式内的 `term` 是策略证明时，
关键字 `from` 可被省略。

```lean {wrapper=false, lineNos=false}
term ::= ...
  | show term by tacticSeq
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="类型注解用在证明里"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类型注解用在证明里" 
  open=false
>}}
上述例子无法正常执行策略风格证明，
因为 Lean 无法推断出用户期待证明的命题。
在运行前方的策略时，
命题会被自动细化 refine 为一个可被策略证明的命题。
然而默认情况下它会被细化为一个错误的命题，
从而导致证明失败。

```lean {wrapper=false, lineNos=false}
example (n : Nat) := by
  induction n
  next => rfl
  next n' ih =>
    simp only [HAdd.hAdd, Add.add, Nat.add] at *
    rewrite [ih]
    rfl
-- Invalid rewrite argument: Expected an
--   equality or
--   iff proof or
--   definition name, 
-- but `ih` is a proof of
--   0 ≍ n'
```

期待被证明的命题可通过 `show` 来进行类型前缀注解。
在某些语法语境中，如果添加局部声明的代价很大，
那么类型前缀注解就可以排上用场：

```lean {wrapper=false, lineNos=false}
example (n : Nat) := show 0 + n = n by
  induction n
  next => rfl
  next n' ih =>
    simp only [HAdd.hAdd, Add.add, Nat.add] at *
    rewrite [ih]
    rfl
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="类型注解用在 `do` 代码块里"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类型注解用在 `do` 代码块里" 
  open=false
>}}
下述例子缺乏足够的类型信息来推断 `Pure` 实例。

```lean {wrapper=false, lineNos=false}
example := do
  return 5
-- typeclass instance problem is stuck
--   Pure ?m.12
-- 
-- Note: Lean will not try to resolve this typeclass instance problem 
-- because the type argument to `Pure` is a metavariable. 
-- This argument must be fully determined 
-- before Lean will try to resolve the typeclass.
-- 
-- Hint: Adding type annotations and supplying implicit arguments to functions 
-- can give Lean more information for typeclass resolution. For example, 
-- if you have a variable `x` that you intend to be a `Nat`, 
-- but Lean reports it as having an unresolved type like `?m`, 
-- replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
```

使用 `show` 的类型前缀注解与
`hole` 连用
可以用来指明单子。
默认的 `OfNat _ 5` 实例提供的类型信息
足以将 `hole` 自动填充为 `Nat`。

```lean {wrapper=false, lineNos=false}
example := show StateM String _ from do
  return 5
```
{{< /admonition >}}

类型前缀注解和
`show` 之间有个很重要的差异：
普通的类型后缀注解改变了项的预期类型，
这可能会改变项的阐述方式；在被阐述后 Lean 
  会推断出结果项的类型，并
  将被推断出的类型用于后续的阐述任务。
另一方面，`show` 会阐述为一个项，
其推断出的类型就是被注解的类型。
[广义字段表示法](https://lean-lang.org/doc/reference/latest/Terms/Function-Application/#--tech-term-generalized-field-notation)
可以用来观察到这样的差异，其中被注解的类型
只有在使用 `show` 时才会被用于解析字段。

{{< labelindex 
  type="例子" 
  summary="类型前缀、后缀注解影响代码结果"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类型前缀、后缀注解影响代码结果" 
  open=false
>}}
下述定义为 `List String` 构建了一个别名：

```lean {wrapper=false, lineNos=false}
def Colors := List String
```

尽管类型后缀注解提供了必要的类型信息
来确定 `List.nil` 的隐式参数 `String`，
但是最终推导出的类型依然是 `List String`：

```lean {wrapper=false, lineNos=false}
#check ([] : Colors)
-- [] : List String
```

相反如果用的是 `show`，
那么待阐述的项在构建时类型就会被推断为 `Colors`：

```lean {wrapper=false, lineNos=false}
#check (show Colors from [])
-- have this := [];
-- this : Colors
```

下述函数被设计成通过[广义字段表示法](https://lean-lang.org/doc/reference/latest/Terms/Function-Application/#--tech-term-generalized-field-notation)来调用：

```lean {wrapper=false, lineNos=false}
def Colors.hasYellow (cs : Colors) : Bool :=
  cs.any (·.toLower == "yellow")
```

由于类型推断结果不同，它
  不能与类型后缀注解一起使用，但
  可以与 `show` 一起使用。

```lean {wrapper=false, lineNos=false}
#eval ([] : Colors).hasYellow
-- Invalid field `hasYellow`: The environment 
-- does not contain `List.hasYellow`, so 
-- it is not possible to project the field `hasYellow` 
-- from an expression
--   []
-- of type `List String`

#eval (show Colors from []).hasYellow
-- false
```
{{< /admonition >}}

## 索引 Index {#index}

### 语法

{{< indexlist type="语法" >}}

### 常量

{{< indexlist type="常量" code_wrap=true  >}}

### 选项

{{< indexlist type="选项" code_wrap=true >}}

### 属性

{{< indexlist type="属性" code_wrap=true >}}

### 例子

{{< indexlist type="例子" print_section=false >}}


---

> 作者: [沉积岩](ych817.github.io)  
> URL: https://ych817.github.io/posts/94de0a1/