[Agda] Raw natural numbers

[Alan Jeffrey]

Building compiler... fingers crossed...

On 10/29/2010 02:52 AM, Ulf Norell wrote:
>
> On Thu, Oct 21, 2010 at 8:44 PM, Alan Jeffrey <ajeffrey at bell-labs.com
> <mailto: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