[Agda] tuple patterns

[Serge D. Mechveliani]

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)
is easier to write/read than

  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