[Agda] Short proof of falsity

[Paul van der Walt]

The first thing that comes to mind is that your Nat is weird -
why should zero take an argument?

Also, this example doesn't work if you remove the BUILTIN
NATURAL, because you can't construct an inhabitant of ℕ. The
only thing that's "broken" here is that maybe the pragma should
be more strict in what it accepts, but that's why you're able to
prove bottom.

Also, it's unclear if that's even what you mean by this code
snippet, since it lacks an explanation.

Cheers
Paul

On Wed, Apr 18, 2012 at 16:01:12 +0100, quoth Anton Setzer:
> > module strangeNat where
> Anton and Karim
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 836 bytes
Desc: Digital signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120418/4dac7af5/attachment.bin