From b43f13c9a93328df6f783394d222f991dc19584c Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Sun, 20 Mar 2022 00:20:46 +0000 Subject: [PATCH] Doc changes from Ralf --- docs/resource_algebras.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md index 8514d92d6..eed48bbf6 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 -- GitLab