[Agda] Interfacing with Haskell

[Ivan Tomac]

Nils Anders Danielsson wrote:
>
> 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?
>

Yes, that's a much better way of phrasing what I'm after.

> 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₂ = …
>

Oh, right. That should make things easier.
Is there a document somewhere describing Agda grammar by the way?