Agda-2.3.2.2: test/epic/Prelude/Bot.agda

module Prelude.Bot where

data Bot : Set where

magic : ∀{A : Set} -> Bot -> A
magic ()