Commit 1b56406c authored by Ralf Jung's avatar Ralf Jung

clarify inG comment; fix subG instance name

parent 46087950
...@@ -4,7 +4,7 @@ Import uPred. ...@@ -4,7 +4,7 @@ Import uPred.
(** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors (** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
[Σ]. This class is similar to the [subG] class, but written down in terms of [Σ]. This class is similar to the [subG] class, but written down in terms of
individual CMRAs instead of lists of CMRA functors. This additional class is individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
needed because Coq is otherwise unable to solve type class constraints due to needed because Coq is otherwise unable to solve type class constraints due to
higher-order unification problems. *) higher-order unification problems. *)
Class inG (Σ : gFunctors) (A : cmraT) := Class inG (Σ : gFunctors) (A : cmraT) :=
......
...@@ -101,7 +101,7 @@ Proof. ...@@ -101,7 +101,7 @@ Proof.
move=> H i; move: H=> /(_ i) [j ?]. move=> H i; move: H=> /(_ i) [j ?].
exists (Fin.L _ j). by rewrite /= fin_plus_inv_L. exists (Fin.L _ j). by rewrite /= fin_plus_inv_L.
Qed. Qed.
Instance inGF_app_r Σ Σ1 Σ2 : subG Σ Σ2 subG Σ (gFunctors.app Σ1 Σ2). Instance subG_app_r Σ Σ1 Σ2 : subG Σ Σ2 subG Σ (gFunctors.app Σ1 Σ2).
Proof. Proof.
move=> H i; move: H=> /(_ i) [j ?]. move=> H i; move: H=> /(_ i) [j ?].
exists (Fin.R _ j). by rewrite /= fin_plus_inv_R. exists (Fin.R _ j). by rewrite /= fin_plus_inv_R.
......
Markdown is supported
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