Unverified Commit 52cc8130 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Sketch some docs.

parent 58dceea1
Pipeline #63485 passed with stage
in 8 minutes and 31 seconds
......@@ -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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment