------------------------------------------------------------------------ -- Empty type ------------------------------------------------------------------------ {-# OPTIONS --universe-polymorphism #-} module Data.Empty where open import Level data ⊥ : Set where {-# IMPORT Data.FFI #-} {-# COMPILED_DATA ⊥ Data.FFI.AgdaEmpty #-} ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever ⊥-elim ()