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

Style fixes from review

parent a030dceb
......@@ -275,8 +275,9 @@ your example would look as follows:
```coq
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.
Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * )))].
Instance subG_libΣ {Σ} : subG libΣ Σ libG Σ.
Proof. solve_inG. Qed.
```
......
......@@ -6,9 +6,10 @@ From iris.prelude Require Import options.
Import uPred.
Class cinvG Σ := cinv_inG : inG Σ fracR.
Definition cinvΣ : gFunctors := #[GFunctor fracR].
Local Existing Instance cinv_inG.
Definition cinvΣ : gFunctors := #[GFunctor fracR].
Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ cinvG Σ.
Proof. solve_inG. Qed.
......
......@@ -29,8 +29,8 @@ From iris.prelude Require Import options.
(* The uCMRA we need. *)
Class gset_bijG Σ A B `{Countable A, Countable B} :=
GsetBijG { gset_bijG_inG : inG Σ (gset_bijR A B); }.
Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
Local Existing Instance gset_bijG_inG.
Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
#[ GFunctor (gset_bijR A B) ].
......
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