Vincent Siles (Nov 23 2021 at 17:00): 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: Oct 13 2024 at 01:02 UTC