最も基本的な関数抽象では関数のパラメータを表す変数を導入します：
term ::= ... | fun ident => term
エラボレーション時に、Lean は関数の定義域を決定できなければなりません。type ascription はこの情報を提供する1つの方法です：
term ::= ... | fun ident : term => term
6.3. 関数（Functions）
関数型を持つ項は Lean.Parser.Term.fun : termfun キーワードで導入される抽象化によって作成することができます。 多くのコミュニティでは、関数抽象は Alonzo Church の記法に由来する ラムダ式 （lambda）や、これがグローバル環境で名前を与えて定義する必要がないことから 匿名関数 （anonymous function）とよばれます。 コア型理論の抽象化では1つの変数しか束縛できませんが、高レベルの Lean での構文では関数項は非常に柔軟です。
syntaxFunction Abstraction
Lean.Parser.Command.definition : commanddef のようなキーワードで定義された関数定義は Lean.Parser.Term.fun : termfun に脱糖されます。一方、帰納型の宣言は Lean.Parser.Term.fun : termfun だけでは実装できない関数型（コンストラクタと型コンストラクタ）を持つ新しい値を導入します。
syntaxCurried Functions
Lean.Parser.Term.fun : termfun の後に複数のパラメータ名を指定することができます：
term ::= ... | fun ident ident* => term
term ::= ... | fun ident ident* : term => term
複数のパラメータに対して異なる型注釈を付けるには、括弧が必要です：
term ::= ... | fun (ident* : term) =>term
これらは Lean.Parser.Term.fun : termfun 項を入れ子にして書くことと同じです。
本節で説明するすべての構文において Lean.Parser.Term.fun : term=> は Lean.Parser.Term.fun : term↦ に置き換えることができます。
関数抽象では、パラメータ指定の一部としてパターンマッチ構文を使用することもでき、すぐに分解されてしまうローカル変数をわざわざ導入する必要性を避けることができます。この構文は パターンマッチの節 で説明されています。
6.3.1. 暗黙のパラメータ（Implicit Parameters）
Lean は関数への暗黙のパラメータをサポートしています。これはユーザが必要な引数をすべて与えるのではなく、Lean 自身が関数に引数を与えられることを意味します。暗黙のパラメータには3種類あります：
- 通常の暗黙のパラメータ
通常の 暗黙 （implicit）のパラメータは、Lean が単一化によって値を決定すべき関数パラメータです。言い換えると、各呼び出し位置において、関数呼び出し全体が well-typed な潜在的な引数値を1つだけ持つべきです。Lean エラボレータは関数の各出現に対してすべての暗黙の引数の値を見つけようとします。通常の暗黙のパラメータは波括弧（
{と}）で囲んで記述します。
- 厳密な暗黙のパラメータ
厳密な暗黙 （strict implicit）なパラメータは通常の暗黙のパラメータと同じですが、Lean は呼び出し先で明示的な引数が指定された場合にのみ引数の値を見つけようとします。厳密な暗黙のパラメータは二重の波括弧（
⦃と⦄、もしくは{{と}}）で記述します。
- インスタンス暗黙のパラメータ
インスタンス暗黙 （instance implicit）のパラメータは 型クラス統合 を介して見つかります。インスタンス暗黙のパラメータは大括弧（
[と]）で囲まれます。他の種類の暗黙のパラメータとは異なり、インスタンス暗黙のパラメータは:無しで記述され、名前を指定するのではなく、パラメータの型を指定します。さらに、単一の名前しか許されません。関数のパラメータとして統合されたインスタンスは、明示的に名前をつけなくても関数の本体ですでに利用可能であるため、ほとんどのインスタンス暗黙のパラメータはパラメータ名を省略します。
通常と厳密な暗黙のパラメータ
f と g の違いは、 f では α が厳密に暗黙であることです：
def f ⦃α : Type⦄ : α → α := fun x => x
def g {α : Type} : α → α := fun x => x
これらの関数は具体的な引数に適用される際にも同じものとしてエラボレートされます：
example : f 2 = g 2 := rfl
しかし、明示的な引数が与えられない場合、 f の使用は暗黙の α を解決する必要はありません：
example := f
一方で、g を利用する際はその解決を要求し、利用可能な情報が不十分な場合はエラボレートに失敗します：
example := g
don't know how to synthesize implicit argument 'α' @g ?m.6 context: ⊢ Type
syntaxFunctions with Varying Binders
Lean.Parser.Term.fun : termfun の最も一般的な構文では、束縛子のシーケンスを受け入れます：
term ::= ... | fun funBinder funBinder* => term
syntaxFunction Binders
関数の束縛子には以下のいずれかの形式が可能です。単一の識別子：
funBinder ::= ... | ident
括弧をつけた識別子の列：
funBinder ::= ...
| Parentheses, used for grouping expressions (e.g., `a * (b + c)`).
Can also be used for creating simple functions when combined with `·`. Here are some examples:
- `(· + 1)` is shorthand for `fun x => x + 1`
- `(· + ·)` is shorthand for `fun x y => x + y`
- `(f · a b)` is shorthand for `fun x => f x a b`
- `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
- also applies to other parentheses-like notations such as `(·, 1)`
type ascription の付いた識別子の列：
funBinder ::= ...
| Type ascription notation: `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
An empty type ascription `(e :)` elaborates `e` without the expected type.
This is occasionally useful when Lean's heuristics for filling arguments from the expected type
do not yield the right result.
type ascription が有る・無い暗黙のパラメータ：
funBinder ::= ...
| 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.
funBinder ::= ...
| 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.
無名・命名されたインスタンス暗黙：
funBinder ::= ...
| 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.
funBinder ::= ...
| 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.
type ascription が有る・無い厳密な暗黙のパラメータ：
funBinder ::= ...
| 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.
funBinder ::= ...
| 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.
通常通り、識別子の代わりに _ を使って無名のパラメータを作成することができ、 ⦃ と ⦄ はそれぞれ {{ と }} を使って書くことができます。
Lean のコア言語では暗黙・インスタンス暗黙・明示的なパラメータを区別しません：様々な種類の関数と関数型は definitionally equal です。これらの違いはエラボレーション時においてのみ観測されます。
関数の型に暗黙のパラメータが含まれており、束縛子には含まれていない場合、結果の関数にはコードで示された束縛子よりも多くのパラメータが含まれるようになる場合があります。これは暗黙のパラメータが自動的に追加されるためです。
型の暗黙のパラメータ
恒等関数は1つの明示的なパラメータで書くことができます。型が既知である限り、暗黙の型パラメータは自動的に追加されます。
#check (fun x => x : {α : Type} → α → α)
fun {α} x => x : {α : Type} → α → α
下記はすべて同等です：
#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} → α → α