Since Agda is intuitionistic one has to postulate the law of excluded middle. But as far as I know, intuitionistic logic accepts ex falso quodlibet or the principle of explosion (the theorem that everything follows from absurdity). How can one prove this postulate:
data ⊥ : Set where
postulate exp : ∀ {n} {x : Set n} → ⊥ → x
One can prove the principle of explosion as follows
data ⊥ : Set where
exp : ∀ {n} {x : Set n} → ⊥ → x
exp ()
If one does not know how to prove this, one may start with a hole:
data ⊥ : Set where
exp : ∀ {n} {x : Set n} → ⊥ → x
exp absurd = {! !}
Then, in emacs agda2-mode one can press C-c C-l to typecheck, so that hole will be replaced and emacs will show the target. In this case target is of type .x. Then one can click on that hole and press C-c C-c and type absurd to split this function by variable absurd. Emacs will produce the final result as given above.