Merge branch 'robbert/countable_eq_dec' into 'master'

Comment about `EqDecision` in `Countable`.

See merge request !268

theories/countable.v

@@ -3,6 +3,11 @@ From stdpp Require Export list numbers list_numbers fin.
 From stdpp Require Import options.
 Local Open Scope positive.
 
+(* Note that [Countable A] gives rise to [EqDecision A] by checking equality of
+the results of [encode]. This instance of [EqDecision A] is very inefficient, so
+the native decider is typically preferred for actual computation. To avoid
+overlapping instances, we include [EqDecision A] explicitly as a parameter of
+[Countable A]. *)
 Class Countable A `{EqDecision A} := {
   encode : A → positive;
   decode : positive → option A;