# [Agda] tuple patterns

Serge D. Mechveliani mechvel at botik.ru
Fri Sep 21 21:18:41 CEST 2012

People,
I have the three simple questions on the syntax, and a minor note on
the type denotations.

I. Is it reliable to write  ->  instead of  \arrow ?

II. Tuple patterns.

Writing nested with' often reduces readability.
So I try tuple patterns, similar as in Haskell. For example,

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

(For this letter I replace  \bn -> Nat,  \<=  ->  <=,  \lambda -> \lam).

And it is not parsed in  Agda-2.3.0.1.

I expect that with' is a language construct, and case' is a library
function (are they?).
Still, as I failed with with', I try case'. The only variant that I
have found working was

f m = let pair : Dec (3 <= m ) x Dec (m <= 6)
pair = (3 <=? m , m <=? 6)
in
case pair of \lam { (no _ , _    ) -> 1
; (_ ,    yes _) -> 2
; _              -> 3
}
1. How accomodate with' to this tuple usage?
2. How to avoid introducing an extra variable (pair') ?
(no matter in with' or in case').
For example, I expect that
case  ((3 <=? m , m <=? 6)  : Dec (3 <= m) x Dec (m <= 6))  of \lam
{ ... }
will not work.

III. In-place type denotations.

For example, the expression
f ((1 , 2) : Nat x Nat) ((3 , 4) : Nat x Nat)

let p1 : Nat x Nat
p1 = (1 , 2)
p2 : Nat x Nat
p2 = (1 , 2)
in  f p1 p2

(two variables introduced, and 4 extra lines).
It is desirable for the language and compiler to allow the former.

Thank you in advance for explanation,

-------
Sergei
`