-- The empty type; also used as absurd proposition (``Falsity'').

{-# OPTIONS --without-K --safe #-}

module Tools.Empty where

data  : Set where

-- Ex falsum quod libet.

⊥-elim :  {a} {A : Set a}    A
⊥-elim ()