[Agda] tuple patterns

Nils Anders Danielsson nad at chalmers.se
Sat Sep 22 13:36:21 CEST 2012

On 2012-09-22 11:39, Serge D. Mechveliani wrote:
> I meant:
>    I write  ->  instead of the math symbol; the compiler takes it,
>    but I wonder whether the Language allows this.

It does, -> and → are lexed into the same token, as are forall and ∀,
and \ and λ.

> And if the first pattern  ``... | no p''  shoots at run time, I need
> ``orderedList? (y :: xs)''  not to evaluate here -- by laziness
> (which laziness is used here for optimization). Is this reliable in
> Agda ?

I'm not sure how parallel withs are translated into the internal
language. The MAlonzo backend compiles via Haskell, which presumably
gives you the right behaviour. Perhaps you get the right behaviour with
the other backends as well; one option is to inspect the generated


More information about the Agda mailing list