[Agda] {} for nested `with' syntax

[Sergei Meshveliani]

Dear Agda developers,

A nested `with' construct often requires repeating a large pattern, so
that a program becomes difficult to read. For example, the fragment

 
-----------------------------------------------------------------
f : ∀ a b e → (add (a , e) ∘ add(b , e)) ≈∘ (add (a + b , e))

f a b e []  with compare e e
... |
      tri≈ _    _ _    = =ms-refl
... | tri< e<e' _ _    = ⊥-elim ..
... | tri> _    _ e>e' = ⊥-elim ..

f a b e ((c , e₁) ∷ mons)  with compare e e₁    -- I
...
    | tri> _ _ _ with compare e e
...        | tri≈ _    _ _    = =ms-refl
...        | tri< e<e' _ _    = ..
...        | tri> _    _ e>e' = ..

f a b e ((c , e₁) ∷ mons)                       -- II
    | tri≈ _ _ _
                 with compare e e
...        | tri≈ _ _ _       = ..
...        | tri< e<e' _ _    = ..
...        | tri> _    _ e>e' = ..
-------------------------------------------------------------------

repeats the pattern 
            f a b e ((c , e₁) ∷ mons)     -- (P)

And in practice, larger patterns are repeated.

Suppose that the {} syntax is added to `with'.
Then the part  (I) + (II)  can be written without repeating (P):


f a b e ((c , e₁) ∷ mons)  with compare e e₁
...
    | tri> _ _ _ with compare e e
           {...        | tri≈ _    _ _    = =ms-refl
            ...        | tri< e<e' _ _    = ..
            ...        | tri> _    _ e>e' = ..
           }
... | tri≈ _ _ _ with compare e e
           {...        | tri≈ _ _ _       = ..
            ...        | tri< e<e' _ _    = ..
            ...        | tri> _    _ e>e' = ..
           }

What is your opinion?

Regards,

------
Sergei