[Agda] Interfacing with Haskell

[Nils Anders Danielsson]

On 2009-11-22 23:41, Ivan Tomac wrote:
> Oh, right. Is there a way to map the whole range of Int-s to some type 
> in Agda? So that in the compiled code (suc zero) gets replaced with 1 
> for example.

I am not sure exactly what you want to do. Do you want to use unary
natural numbers in Agda, but machine integers in the compiled program?
Do you also want to use fast algorithms taking advantage of the
non-unary representation of the machine integers?

By the way, for most purposes I would recommend using Integer rather
than Int.

> I forgot to mention I tried that too. I couldn't figure out how to get 
> that to work with more than one expression.

f p with e₁ | e₂
... | p₁ | p₂ = …

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.