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

Use new style for `inG` instances in docs as well

parent 9c0037c6
......@@ -99,9 +99,10 @@ for further details on `libG` classes). For example, the STS library is
parameterized by an STS and assumes that the STS state space is inhabited:
```coq
Class stsG Σ (sts : stsT) := {
sts_inG :> inG Σ (stsR sts);
sts_inG : inG Σ (stsR sts);
sts_inhabited :> Inhabited (sts.state sts);
}.
Local Existing Instance sts_inG.
```
In this case, the `Instance` for this `libG` class has more than just a `subG`
assumption:
......
......@@ -14,7 +14,8 @@ Libraries typically bundle the `inG` they need in a `libG` typeclass, so they do
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 }.
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,
......@@ -273,8 +274,9 @@ Putting it all together, the `libG` typeclass and `libΣ` list of functors for
your example would look as follows:
```coq
Class libG Σ := { lib_inG :> inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
Class libG Σ := { lib_inG : inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * )))].
Local Existing Instance lib_inG.
Instance subG_libΣ {Σ} : subG libΣ Σ libG Σ.
Proof. solve_inG. Qed.
```
......
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