[Agda] "with" notation?

[Randy Pollack]

I have a syntax problem, so consider the following example without
caring about the actual types and constructors:

Map-minus : (m n : <Map>) -> Maybe <Map>
Map-minus n map_zro = just n
Map-minus (map_pos (pmap_c m1 m2)) (map_pos (pmap_l n')) with
    Map-minus (map_pos m1) (map_pos n')
... | just m = just (Map_c m (map_pos m2))
... | nothing = nothing
Map-minus (map_pos (pmap_c m1 m2)) (map_pos (pmap_c n1 n2)) with
    (Map-minus (map_pos m1) (map_pos n1), Map-minus (map_pos m2) (map_pos n2))
... | (_ , _) = nothing

In the (trivial) last case, I want to use the "with" notation on two
patterns.  I couldn't figure out the syntax for two patterns, so I
tried to make a single pattern by pairing.  This failed

/home/rpollack/work/binding/nominalIsabelle/sato/injective/second/Abst.agda:105,1-108,24
Not implemented: Pattern matching for records
when checking that the clause
.Abst.with-71 m1 m2 n1 n2 (_ , _) = nothing has type
(m1 : <PMap>) (m2 : <PMap>) (n1 : <PMap>) (n2 : <PMap>)

BTW, I'm using a version of Agda I downloaded yesterday
    apt-get install agda-mode 

Thanks,
Randy

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.