Stream: Coq users

Topic: stdpp: mapM more friendly to gmap ?


view this post on Zulip Vincent Siles (Nov 23 2021 at 17:00):

I'm trying to use mapM with a stringmap A, with something like

Definition map_args {A B: Type} (f: A  option  B) (m: stringmap A) : option (stringmap B) :=
  let g (x: (string * A)) := f x.2 = (fun y => mret (x.1, y)) in
  mapM g (map_to_list m) = (fun l => mret (list_to_map l))

This works fine, but I have a hard time getting this to work with lookup. The only lemmas I found so far were mapM_Some that gives me a Forall2, but this one indexes lists with nth, not fin_maps.

I am missing something, or should I build something like this for associativity lists / stringmaps ?


Last updated: Feb 01 2023 at 11:04 UTC