------------------------------------------------------------------------
-- The Agda standard library
--
-- Level polymorphic Empty type
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Empty.Polymorphic where
import Data.Empty as Empty using (⊥; ⊥-elim)
open import Level using (Level; Lift; _⊔_)
⊥ : {ℓ : Level} → Set ℓ
⊥ {ℓ} = Lift ℓ Empty.⊥
-- make ⊥-elim dependent too, as it does seem useful
⊥-elim : ∀ {w ℓ} {Whatever : ⊥ {ℓ} → Set w} → (witness : ⊥ {ℓ}) → Whatever witness
⊥-elim ()
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4