13.2. 函数类型🔗

Lean 的函数类型所描述的不只是函数的定义域和值域。它们还为应用处的精译提供指令：某些参数应通过合一或类型类合成自动确定，某些参数是带默认值的可选参数，还有一些参数应使用自定义策略脚本合成。此外，其语法还支持简写柯里化函数。

语法函数类型

依赖函数类型包含显式名称：

term ::= ...
    | (ident : term) → term

非依赖函数类型则不包含：

term ::= ...
    | term → term

语法柯里化函数类型

依赖函数类型可在同一对圆括号中包含多个类型相同的参数：

term ::= ...
    | (ident* : term) → term

这等价于在嵌套函数类型中为每个参数名称重复类型标注。

语法隐式、可选与自动参数

函数类型可以描述接受隐式参数、实例隐式参数、可选参数和自动参数的函数。除实例隐式参数外，其他参数都要求一个或多个名称。

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

多个同类型参数

Nat.add 的类型可以用以下方式书写：

后两种类型允许用具名实参调用函数；除此之外，三者等价。