Commit bfef1716 authored by Janno's avatar Janno

Add `Countable` instance for `gset`.

parent 25bdb78f
Pipeline #10303 failed with stage
in 0 seconds
......@@ -277,3 +277,7 @@ Proof.
- intros [[m Hm]]; unfold fresh; simpl.
by intros ?; apply (is_fresh (dom Pset m)), elem_of_dom_2 with ().
Qed.
Program Instance gset_countable `{Countable K} : Countable (gset K) :=
inj_countable mapset_car (Some Mapset) _.
Next Obligation. by intros ? ? ? []. Qed.
\ No newline at end of file
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