[Agda] "with" notation?

[Randy Pollack]

Thanks Pierre-Evariste, that works.

I probably should have asked how to write the monadic notation for
passing around objects of the Maybe type.  I only used "with" because
I don't know a better notation.  Please point to an example of this in
the library.

Best,
Randy
--
Pierre-Evariste Dagand writes:
 > 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
 > 

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