From b73e5cb5a2f8db41e1a7b633616402993bd1406f Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 18 Mar 2022 00:32:06 +0100
Subject: [PATCH] Sketch some docs.

---
 docs/resource_algebras.md | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
index 1699a15f5..8514d92d6 100644
--- a/docs/resource_algebras.md
+++ b/docs/resource_algebras.md
@@ -17,10 +17,16 @@ example, in the [one-shot example](../tests/one_shot.v), we have:
 Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
 Local Existing Instance one_shot_inG.
 ```
-The `:>` means that the projection `one_shot_inG` is automatically registered as
-an instance for type-class resolution.  If you need several resource algebras,
-just add more `inG` fields.  If you are using another module as part of yours,
-add a field like `one_shot_other :> otherG Σ`.
+Here, the projection `one_shot_inG` is registered as an instance for type-class
+resolution. If you need several resource algebras, just add more `inG` fields.
+If you are using another module as part of yours, add a field like
+`one_shot_other : otherG Σ`.
+
+The code above enables these typeclass instances only in the surrounding file:
+where they are used to define the new abstraction by the library, while the
+interface of these abstractions will only depend on the `one_shotG` class.
+Since `one_shot_inG` will be hidden from clients, they will not accidentally
+reuse it accidentally in their code.
 
 Having defined the type class, we need to provide a way to instantiate it.  This
 is an important step, as not every resource algebra can actually be used: if
-- 
GitLab