------------------------------------------------------------------------ -- The Agda standard library -- -- Empty type ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Data.Empty where ------------------------------------------------------------------------ -- Definition -- Note that by default the empty type is not universe polymorphic as it -- often results in unsolved metas. See `Data.Empty.Polymorphic` for a -- universe polymorphic variant. data ⊥ : Set where ------------------------------------------------------------------------ -- Functions ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever ⊥-elim ()