[Agda] "with" notation?

[Pierre-Evariste Dagand]

Hi Randy,


According to p.15 of Norell's "Dependently Typed Programming in Agda", this:

> 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

should work once rewritten as:

 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


Cheers,

-- 
Pierre-Evariste