Skip to content

Workaround to avoid `injection` from unfolding equalities on `dom`

Robbert Krebbers requested to merge robbert/injection_gset_dom into master

As reported by @vsiles and @msammler on Mattermost the tactics simplify_eq and injection accidentally unfold equalities dom (gset A) m1 = dom (gset A) m2 into merge ....

The culprit is that the definition of dom on gmap starts with a constructor MapSet. This MR tweaks the definition a bit, by inserting an eta expansion, to avoid that.

Edited by Robbert Krebbers

Merge request reports