依赖函数类型包括显式名称：
term ::= ...
| Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
非依赖函数类型不会：
term ::= ... | term → term
13.2. 功能类型
Lean 的函数类型不仅仅描述函数的域和共域。 它们还提供了详细说明应用程序站点的说明，指示某些参数将通过统一或 类型类合成 自动发现，其他参数是可选的，具有默认值，而其他参数应使用自定义策略脚本进行合成。 此外，它们的语法包含对缩写 curried 函数的支持。
syntaxFunction types
syntaxCurried Function Types
依赖函数类型可以包含在一组括号中具有相同类型的多个参数：
term ::= ...
| Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
这相当于为嵌套函数类型中的每个参数名称重复类型注释。
syntaxImplicit, Optional, and Auto Parameters
函数类型可以描述采用隐式参数、实例隐式参数、可选参数和自动参数的函数。 除实例隐式参数外，所有参数都需要一个或多个名称。
term ::= ...
| Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
term ::= ... |(ident* : term := byExplicit binder, like `(x y : A)` or `(x y)`. Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.tacticSeq) → termA sequence of tactics in brackets, or a delimiter-free indented sequence of tactics. Delimiter-free indentation is determined by the *first* tactic of the sequence.
term ::= ...
| 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.
term ::= ...
| 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.
term ::= ...
| 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.
term ::= ...
| 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.