Commit d0961b67 authored by Robbert Krebbers's avatar Robbert Krebbers

Make `mapset_countable` a global instance.

parent 22e0ade7
...@@ -76,7 +76,7 @@ Section deciders. ...@@ -76,7 +76,7 @@ Section deciders.
match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end); match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
abstract congruence. abstract congruence.
Defined. Defined.
Program Instance mapset_countable `{Countable (M ())} : Countable (mapset M) := Global Program Instance mapset_countable `{Countable (M ())} : Countable (mapset M) :=
inj_countable mapset_car (Some Mapset) _. inj_countable mapset_car (Some Mapset) _.
Next Obligation. by intros ? ? []. Qed. Next Obligation. by intros ? ? []. Qed.
Global Instance mapset_equiv_dec : RelDecision (@{mapset M}) | 1. Global Instance mapset_equiv_dec : RelDecision (@{mapset M}) | 1.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment