6.2. 関数型（Function Types）

Lean の関数型は、関数の定義域と値域以上のものを記述します。関数型はその適用位置をエラボレートするための指示も提供します。これはいくつかのパラメータは単一化または 型クラス統合 によって自動的に検出され、他のパラメータはデフォルトでオプションであり、さらに他のパラメータはカスタムのタクティクスクリプトを使用して統合すべきであることによって示されます。さらに、その構文には カリー化された 関数を省略するためのサポートが含まれています。

syntaxFunction 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)`.
(ident : term) → term

非依存関数型では含まれません：

term ::= ...
    | term → term
syntaxCurried Function Types

依存関数型は、同じ型を持つ複数のパラメータを1つの括弧の中に含めることができます：

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)`.
(ident* : term) → term

これは入れ子になった関数型の各パラメータ名に対して、型注釈を繰り返すことと同じです。

syntaxImplicit, Optional, and Auto Parameters

関数型は暗黙・インスタンス暗黙・オプショナル・自動的なパラメータを取る関数を記述することができます。インスタンス暗黙パラメータを除くすべてのパラメータは1つ以上の名前を必要とします。

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)`.
(ident* : term := term) → term
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)`.
(ident* : term := by A 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. tacticSeq) → term
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.
{ident* : term} → term
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] → term
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.
[ident : term] → term
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.
⦃ident* : term⦄ → term
同じ型の複数のパラメータ

Nat.add の型は以下のように書くことができます：

最後の2つの型は関数を 名前付き引数 と一緒に使うことができます；これを除けばこれら3つはすべて同等です。