[Agda] tuple patterns

[Nils Anders Danielsson]

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
source.

-- 
/NAD