帰納型の知られざる一生
帰納的対象
より精確には、「帰納的宣言」の全体像は型・コンストラクタのリスト・再帰子のリストからなります。宣言の型とコンストラクタはユーザが指定し、再帰子はそれらの要素から派生します。各再帰子は計算規則とも呼ばれる「再帰子規則」のリストも取得します。これはι簡約（パターンマッチの大げさな言い方）で使用される値レベルの式です。これ以降においては、「帰納型」と「帰納的宣言」はなるべく区別するようにします。
Lean のカーネルでは相互帰納的宣言をネイティブにサポートしています。この場合、（型とコンストラクタのリストの）ペアのリストが存在します。カーネルは入れ子になった帰納的宣言について、一時的に相互帰納的宣言に変換することでサポートします（これについては後述します）。
帰納型
カーネルは帰納的宣言のうち「帰納型」について、値ではなく実際に型であることを要求します（infer ty は何らかの sort <n> を生成しなければなりません）。相互帰納型では、宣言される型がすべて同じ宇宙にあり、同じパラメータを持たなければなりません。
コンストラクタ
帰納型のどのコンストラクタにおいても、カーネルによって以下のチェックが課されます：
- コンストラクタの型・テレスコープは宣言されている帰納型と同じパラメータを共有する必要があります。
- コンストラクタ型のテレスコープのパラメータではない要素では、束縛子の型は実際に型でなければなりません（
Sort _として推論されなければなりません）。
- コンストラクタ型のテレスコープのパラメータではない要素では、その要素から推論されたソートが帰納型のソート以下であるか、もしくは帰納型が命題として宣言されていなければなりません。
- コンストラクタの引数は宣言されている型の positive ではない出現を含んではなりません（この問題についてはより知りたい読者は こちら を参照してください）。
- コンストラクタのテレスコープの終わりは、宣言されている型への引数の有効な適用でなければなりません。例えば、
List.cons ..コンストラクタは.. -> List Aで終わる必要があり、.. -> Natで終わるList.cons ..はエラーになります。
入れ子になった帰納的対象
入れ子になった帰納的対象をチェックするのはとても手間のかかる手順です。まず相互ブロックの中の帰納型の入れ子部分を一時的に特殊化することで相互帰納型の「通常の」（入れ子になっていない）あつまりを持つようにし、特殊化された型をチェックし、それからすべての特殊化を解除してそれらの型を認可します。
次の入れ子構造 Array Sexpr を伴った S 式の定義を考えてみましょう：
inductive Sexpr
| atom (c : Char) : Sexpr
| ofArray : Array Sexpr -> Sexpr
俯瞰的に見ると、入れ子の帰納的宣言をチェックするプロセスには3つのステップがあります：
- 現在の型がネストされている「コンテナ型」を特殊化することによって、入れ子になった帰納的宣言を相互帰納的宣言に変換する。コンテナ型自体が他の型で定義されている場合は、それらの要素も特殊化する必要があります。上の例では、コンテナ型として
Arrayを使用していますが、ArrayはListの用語によって定義されているため、ArrayとListの両方をコンテナ型として扱う必要があります。
- 相互帰納型の通常のチェックと構築の手順を行う。
- 特殊化された入れ子の型をもとの形に戻し（非特殊化）、復帰・非特殊化された宣言を環境に追加する。
この特殊化の例として、上記の入れ子になった帰納的対象 Sexpr は次のように変換されます：
mutual
inductive Sexpr
| atom : Char -> Sexpr
| ofList : ListSexpr -> Sexpr
inductive ListSexpr
| nil : ListSexpr
| cons : Sexpr -> ListSexpr -> ListSexpr
inductive ArraySexpr
| mk : ListSexpr -> ArraySexpr
end
そして、これらの型をチェックする過程で元の帰納的宣言を回復します。より明確にすると、「特殊化」といった場合、上記の新しい ListSexpr 型と ArraySexpr 型は通常の List 型のように任意の型に対して汎用的であることは対照的に、Sexpr のリストと配列としてのみ定義されているという意味で特殊化されています。
再帰子
TBD