ボトム型

定義

module bottom-type where

data ⊥ : Set where

性質

もし⊥型の項を構成できるのであれば、任意の命題を示すことができる。

absurd : ∀ {P : Set} → ⊥ → P
absurd ()

このように、Agdaでは使用できる構成子が存在しないとき、()をパターンとして使うことができる。