diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md index 8514d92d663e3d4951be0f938c563193d9ec1894..eed48bbf62c9d827ddd9195727dd796bb7350872 100644 --- a/docs/resource_algebras.md +++ b/docs/resource_algebras.md @@ -20,13 +20,13 @@ Local Existing Instance one_shot_inG. 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 Σ`. +`one_shot_other : otherG Σ`. All of these fields should be added to the `Local Existing Instances`. -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 +The code above enables these typeclass instances only in the surrounding file +where they are used to define the new abstractions by the library. 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. +rely on it 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