Commit 038f8e0e authored by Robbert Krebbers's avatar Robbert Krebbers

Make instances EqDecision and Countable of gmultiset less eager.

Fix fixes issue #63.
parent 64c3fda3
Pipeline #3634 passed with stage
in 10 minutes and 53 seconds
......@@ -7,14 +7,18 @@ Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
Arguments GMultiSet {_ _ _} _.
Arguments gmultiset_car {_ _ _} _.
Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
Lemma gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
Proof. solve_decision. Defined.
Hint Extern 1 (Decision (@eq (gmultiset _) _ _)) =>
eapply @gmultiset_eq_dec : typeclass_instances.
Program Instance gmultiset_countable `{Countable A} :
Program Definition gmultiset_countable `{Countable A} :
Countable (gmultiset A) := {|
encode X := encode (gmultiset_car X); decode p := GMultiSet <$> decode p
|}.
Next Obligation. intros A ?? [X]; simpl. by rewrite decode_encode. Qed.
Hint Extern 1 (Countable (gmultiset _)) =>
eapply @gmultiset_countable : typeclass_instances.
Section definitions.
Context `{Countable A}.
......
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