The empty type. It has no constructors. The Empty.rec
eliminator expresses the fact that anything follows from the empty type.
12.10. 空の型（The Empty Type）
Planned Content
Tracked at issue #170
空の型 Empty は不可能な値を表します。これはコンストラクタを一切持たない帰納型です。
自明な型 Unit はパラメータを取らないコンストラクタを1つ持ち、結果が不要であったり興味がないような計算をモデル化するために使用することができますが、 Empty は計算が決して可能であってはならない状況で使用することができます。 Empty で多相型をインスタンス化すると、そのコンストラクタの一部（対応する型のパラメータを持つコンストラクタ）を不可能なものとしてマークすることができます；これによってコード中の望ましくないパスを除外することができます。
Empty 型を持つ項が出現した場合、不可能なコードパスに到達したことを示します。コンストラクタがないため、この型の値が存在することはありません。不可能なコードパスでは、それ以降のコードを書くすべがありません； Empty.elim 関数を使用することで、不可能なパスから抜け出すことができます。
inductive type
Empty : Type
inductive type
PEmpty.{u} : Sort u
The universe-polymorphic empty type. Prefer Empty or False where
possible.
Constructors
不可能なコードパス
関数 f のシグネチャは例外を投げる可能性を示していますが、例外の型は何でも良いです：
def f (n : Nat) : Except ε Nat := pure n
f の例外の型を Empty でインスタンス化することで、 f が実際に決して例外を投げないことを利用して、例外が投げられないことを型が示す関数に変換します。特に、 Empty.elim を使用することで、不可能な例外の値を渡さないようにすることができます。
def g (n : Nat) : Nat :=
match f (ε := Empty) n with
| .error e =>
Empty.elim e
| .ok v => v
12.10.1. API リファレンス（API Reference）
def
Empty.elim.{u} {C : Sort u} : Empty → C
Empty.elim : Empty → C says that a value of any type can be constructed from
Empty. This can be thought of as a compiler-checked assertion that a code path is unreachable.
This is a non-dependent variant of Empty.rec.