Agda-2.3.2.2: test/succeed/AbsurdPattern.agda
-- Pattern matching on a (decidably) empty type allows you to omit the
-- right-hand side.
module AbsurdPattern where
data Empty : Set where
elim-Empty : {A : Set} -> Empty -> A
elim-Empty ()
-- Pattern matching on a (decidably) empty type allows you to omit the
-- right-hand side.
module AbsurdPattern where
data Empty : Set where
elim-Empty : {A : Set} -> Empty -> A
elim-Empty ()