module empty where ---------------------------------------------------------------------- -- datatypes ---------------------------------------------------------------------- data ⊥ : Set where ---------------------------------------------------------------------- -- syntax ---------------------------------------------------------------------- ---------------------------------------------------------------------- -- theorems ---------------------------------------------------------------------- ⊥-elim : ⊥ → ∀ {P : Set} → P ⊥-elim ()