[Agda] Raw natural numbers

[Ulf Norell]

On Thu, Oct 21, 2010 at 8:44 PM, Alan Jeffrey <ajeffrey at bell-labs.com>wrote:

> I'm building the new compiler now...  Fingers crossed!
>
> A more general solution to the problem of unsafeCoerce getting in the way
> would be for Agda to use its own coerce function, defined something like:
>
>  {-# INLINE [1] coerce #-}
>  coerce = Unsafe.Coerce.unsafeCoerce
>
>  {-# RULES "coerce-id" forall (x :: a) . coerce x = x #-}
>
> This would at least remove all the identity coercions, and would allow
> other FFI bindings to define their own RULES.


I've pushed a patch that does this. Let me know how it works out.

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