[Agda] tuple patterns

[Serge D. Mechveliani]

On Fri, Sep 21, 2012 at 09:42:29PM +0200, Nils Anders Danielsson wrote:
> On 2012-09-21 21:18, Serge D. Mechveliani wrote:
>> I. Is it reliable to write  ->  instead of  \arrow ?
>
> If you've encountered a problem, please report a bug.

I meant: 
  I write  ->  instead of the math symbol; the compiler takes it,
  but I wonder whether the Language allows this.

>>    f : Nat -> Nat
>>    f m   with  (3 <=? m , m <=? 6)    -- : Dec (3 <= m) x Dec (m <= 6)
>>    ... | (no _ , _    ) = 1
[..]

> In this case I suggest that you use the following notation instead,
> though:
>
>   f : Nat -> Nat
>   f m with 3 <=? m | m <=? 6
>   ... | no _ | _     = 1
> [..]

Good. Thank you. 
I write now
 ...
 orderedList? (x :: y :: xs)   with  x <=? y | orderedList? (y :: xs)

 ... | no  p    | _            =  no (compose p oList-1<=2)
 ... | _        | no  p        =  no (compose p tailOrdered)
 ... | yes x<=y | yes ord-y:xs =  yes $ prep2 x y xs x<=y ord-y:xs

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 ?

Thanks,

-------
Sergei