Skip to content

Stronger version of `gmap_core_id`.

Robbert Krebbers requested to merge robbert/gmap_core_id into master

To obtain CoreId m where m : gmap K A, the prior version requires CoreId to hold for all values x : A. The new version only requires it to hold for values that are in the map, i.e., with m !! i = Some x.

Since the condition m !! i = Some x is useless for type classes, I made a primed version gmap_core_id' without that condition, and declared that as an instance.

Merge request reports