[Agda] tuple patterns

[Alan Jeffrey]

On 09/22/2012 06:36 AM, Nils Anders Danielsson wrote:
> On 2012-09-22 11:39, Serge D. Mechveliani wrote:
>> 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.

The JS backend is strict. It will fully evaluate with-expressions before 
any pattern-matching.

A.