[Agda] Erasable vs. irrelevant

[jleivent at comcast.net]

Thanks again, Andreas.

> Unless you add an induction axiom (scheme) or at least case distinction, 
> there is no means of definition any function, like addition etc., hence, 
> no computational content in N.

See the enclosed module.  So, even with induction and cases, it still looks to me like it is erasable - or, as you say, that there is no computational content in N.  It is surprising to me that so much about the naturals could be devoid of computational content.  I have a hard time believing that this is correct - but I don't see anything wrong with it.

-- Jonathan Leivent
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Erasable.agda
Type: application/octet-stream
Size: 2349 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20120119/10b756c4/Erasable.obj