More general definition of `big_opM`
Currently, big_opM
is defined in iris/algebra/big_op.v
using:
Local Definition big_opM_def {M : ofe} {o : M → M → M} `{!Monoid o} `{Countable K} {A} (f : K → A → M)
(m : gmap K A) : M := big_opL o (λ _, uncurry f) (map_to_list m).
which means that big_opM
is hard-coded to using gmap
. I'm wondering: why not any map type?
For instance, one could define it as
Local Definition big_opM_def {M : ofe} {o : M → M → M} `{!Monoid o} `{FinMap K MM} {A} (f : K → A → M)
(m : MM A) : M := big_opL o (λ _, uncurry f) (map_to_list m).
or as
Local Definition big_opM_def {M : ofe} {o : M → M → M} `{!Monoid o} {A} `{MapFold K A MM} (f : K → A → M)
(m : MM) : M := big_opL o (λ _, uncurry f) (map_to_list m).
and then tweak the rest of the file, so that big_opM
lemmas can basically work with any FinMap
, not just gmap
.