Skip to content

Misc setoids lemmas and tweaks for maps and option

Robbert Krebbers requested to merge robbert/map_setoid into master
  • Add lemmas map_singleton_equiv_inj and map_fmap_equiv_inj.
  • Add lemma option_fmap_equiv_inj.
  • Add Propers for maps, and generalize existing ones. Add tests to check that the old ones can be derived.
  • Add lemma map_equiv_lookup_r.
  • Add lemma map_equiv_iff.

Also, rename instances option_mbind_proper → option_bind_proper and option_mjoin_proper → option_join_proper to be consistent with similar instances for sets and lists.

Merge request reports