From a762d18345a33fb83c76b6e5fc3f6367314dac83 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 20 Jan 2021 11:10:13 +0100 Subject: [PATCH] Also update docs. --- docs/proof_guide.md | 10 +++++----- docs/resource_algebras.md | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/docs/proof_guide.md b/docs/proof_guide.md index cc1f820b3..284575f87 100644 --- a/docs/proof_guide.md +++ b/docs/proof_guide.md @@ -107,8 +107,8 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension ### small letters -* a : A = cmraT or ofeT -* b : B = cmraT or ofeT +* a : A = cmra or ofe +* b : B = cmra or ofe * c * d * e : expr = expressions @@ -137,8 +137,8 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension ### capital letters -* A : Type, cmraT or ofeT -* B : Type, cmraT or ofeT +* A : Type, cmra or ofe +* B : Type, cmra or ofe * C * D * E : coPset = mask of fancy update or WP @@ -187,5 +187,5 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension * G: global camera functor management (typeclass; see the [resource algebra docs](resource_algebras.md)) * I: bunched implication logic (of type `bi`) * SI: step-indexed bunched implication logic (of type `sbi`) -* T: canonical structures for algebraic classes (for example ofeT for OFEs, cmraT for cameras) +* T: canonical structures for algebraic classes (for example ofe for OFEs, cmra for cameras) * Σ: global camera functor management (`gFunctors`; see the [resource algebra docs](resource_algebras.md)) diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md index 170552701..47553ecfb 100644 --- a/docs/resource_algebras.md +++ b/docs/resource_algebras.md @@ -228,7 +228,7 @@ contractive. To compose these functors, we provide a number of combinators, e.g.: -- `constOF (A : ofeT) : cFunctor := λ (B,Bâ»), A ` +- `constOF (A : ofe) : cFunctor := λ (B,Bâ»), A ` - `idOF : cFunctor := λ (B,Bâ»), B` - `prodOF (F1 F2 : cFunctor) : cFunctor := λ (B,Bâ»), F1 (B,Bâ») * F2 (B,Bâ»)` - `ofe_morOF (F1 F2 : cFunctor) : cFunctor := λ (B,Bâ»), F1 (Bâ»,B) -n> F2 (B,Bâ»)` -- GitLab