From aabff4ca75e1866798d4b545d3bc87046fe81f88 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 May 2021 12:46:31 +0200
Subject: [PATCH] Comment about `EqDecision` in `Countable`.

---
 theories/countable.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/countable.v b/theories/countable.v
index 535d94b2..5573876a 100644
--- a/theories/countable.v
+++ b/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;
-- 
GitLab