Commit 1411b0a9 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Only use Existing Instances.

parent 04b066bc
......@@ -15,12 +15,13 @@ not have to expose to clients what exactly their resource algebras are. For
example, in the [one-shot example](../tests/one_shot.v), we have:
```coq
Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
Local Existing Instance one_shot_inG.
Local Existing Instances 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 Σ`. All of these fields should be added to the `Local Existing Instances`.
`one_shot_other : otherG Σ`. All of these fields should be added to the
`Local Existing Instances` command.
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
......@@ -132,7 +133,7 @@ Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
gen_heap_inG : gen_heapGpreS L V Σ;
gen_heap_name : gname;
}.
Local Existing Instance gen_heap_inG.
Local Existing Instances gen_heap_inG.
```
The trailing `S` here is for "singleton", because the idea is that only one
instance of `gen_heapGS` ever exists. This is important, since two instances
......
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