[Agda] Short proof of falsity

Anton Setzer A.G.Setzer at swansea.ac.uk
Wed Apr 18 17:01:12 CEST 2012


> module strangeNat where
>
> data ℕ : Set where
> zero : ℕ → ℕ
> suc : ℕ → ℕ
>
> data ⊥ : Set where
>
> empty : ℕ → ⊥
> empty (zero y) = empty y
> empty (suc y) = empty y
>
> {-# BUILTIN NATURAL ℕ #-}
>
> p : ⊥
> p = empty 0


Anton and Karim


More information about the Agda mailing list