[Agda] Short proof of falsity

Paul van der Walt paul at denknerd.org
Wed Apr 18 17:11:33 CEST 2012

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.


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

More information about the Agda mailing list