Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]

[Ulf Norell]

On Mon, Apr 23, 2012 at 10:28 AM, Nils Anders Danielsson <nad at chalmers.se>wrote:

> On 2012-04-23 09:07, Andreas Abel wrote:
>
>> Mmh, the easiest fix is: trash the builtin NATDIVSUCAUX. I do not know
>> what it is for. The only use I found for it was in
>>
>>  example/lib/Data/Nat.agda
>>
>> with the definition you have given below.
>>
>
> See http://code.google.com/p/agda/**issues/detail?id=172<http://code.google.com/p/agda/issues/detail?id=172>for some context.
>

The purpose is to give you fast (=running on Haskell integers) div and mod
on nats
at compile time.

By the way, I'm not surprised that people manage to wreak havoc by using
> BUILTINs, in many cases the sanity checking for BUILTINs is less than
> optimal. I think the idea is that you should only use BUILTINs (and
> postulates, and the FFI) if you know what you are doing.


The sanity checking for BUILTINs is supposed to disallow incorrect
definitions,
if it doesn't it's a bug that should be fixed. The FFI and postulates
obviously let
you "prove" whatever you want, but BUILTINs shouldn't.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120423/8b95f3b0/attachment.html