Update CONTRIBUTING.md

1 files changed, 34 insertions, 32 deletions

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 480d330..96c3b76 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -76,7 +76,7 @@ This particular example can be problematic if matrix.v is imported because then,
   + Elements of another ring should be named `x`, `y`, `z`, `u`, `v`, `w`, ...
   + Polynomials should be named by lower case letter `p`, `q`, `r` ... (to avoid collision with properties named `P`, `Q`, ...)
   + Matrices should be named `A`, `B`, ..., `M`, `N`, ...
-  
+
 ### Naming conventions (Non exhaustive)
 #### Names in the library usually obey one of following the convention
  - `(condition_)?mainSymbol_suffixes`
@@ -92,38 +92,40 @@ Or in the presence of a property denoted by a nary or unary predicate:
  - "condition" is used when the lemma applies under some hypothesis.
  - "suffixes" are there to refine what shape and/or what other symbols  the lemma has. It can either be the name of a symbol ("add", "mul",  etc...), or the (short) name of a predicate ("`inj`" for "`injectivity`", "`id`" for "identity", ...) or an abbreviation.
 Abbreviations are in the header of the file which introduce them. We list here the main abbreviations.
-  - A -- associativity, as in `andbA : associative andb.`
-  - AC -- right commutativity.
-  - ACA -- self-interchange (inner commutativity), e.g., `orbACA : (a || b) || (c || d) = (a || c) || (b || d).`
-  - b -- a boolean argument, as in `andbb : idempotent andb.`
-  - C -- commutativity, as in `andbC : commutative andb`,
-    or predicate complement, as in `predC.`
-  - CA -- left commutativity.
-  - D -- predicate difference, as in `predD.`
-  - E -- elimination, as in `negbFE : ~~ b = false -> b`.
-  - F or f -- boolean false, as in `andbF : b && false = false.`
-  - I -- left/right injectivity, as in `addbI : right_injective addb` or predicate  intersection, as in `predI.`
-  - l -- a left-hand operation, as `andb_orl : left_distributive andb orb.`
-  - N or n -- boolean negation, as in `andbN : a && (~~ a) = false.`
-  - n -- alternatively, it is a natural number argument
-  - P -- a characteristic property, often a reflection lemma, as in
+  - `A` -- associativity, as in `andbA : associative andb.`
+  - `AC` -- right commutativity.
+  - `ACA` -- self-interchange (inner commutativity), e.g., `orbACA : (a || b) || (c || d) = (a || c) || (b || d).`
+  - `b` -- a boolean argument, as in `andbb : idempotent andb.`
+  - `C` -- commutativity, as in `andbC : commutative andb`,
+        -- alternatively, predicate or set complement, as in `predC.`
+  - `CA` -- left commutativity.
+  - `D` -- predicate or set difference, as in `predD.`
+  - `E` -- elimination lemma, as in `negbFE : ~~ b = false -> b`.
+  - `F` or `f` -- boolean false, as in `andbF : b && false = false.`
+  - `g` -- a group argument
+  - `I` -- left/right injectivity, as in `addbI : right_injective addb` 
+        -- alternatively predicate or set intersection, as in `predI.`
+  - `l` -- a left-hand operation, as `andb_orl : left_distributive andb orb.`
+  - `N` or `n` -- boolean negation, as in `andbN : a && (~~ a) = false.`
+  - `n` -- alternatively, it is a natural number argument,
+  - `N` -- alternatively ring negation, as in `mulNr : (- x) * y = - (x * y).`
+  - `P` -- a characteristic property, often a reflection lemma, as in
      `andP : reflect (a /\ b) (a && b)`.
-  - r -- a right-hand operation, as `orb_andr : right_distributive orb andb.`
+  - `r` -- a right-hand operation, as `orb_andr : right_distributive orb andb.`
       -- alternatively, it is a ring argument
-  - T or t -- boolean truth, as in `andbT: right_id true andb.`
-  - U -- predicate union, as in `predU`.
-  - W -- weakening, as in `in1W : {in D, forall x, P} -> forall x, P.`
-  - 0 -- ring 0, as in `addr0 : x + 0 = x.`
-  - 1 -- ring 1, as in `mulr1 : x * 1 = x.`
-  - D -- ring addition, as in `linearD : f (u + v) = f u + f v.`
-  - B -- ring subtraction, as in `opprB : - (x - y) = y - x.`
-  - M -- ring multiplication, as in `invfM : (x * y)^-1 = x^-1 * y^-1.`
-  - Mn -- ring by nat multiplication, as in `raddfMn : f (x *+ n) = f x *+ n.`
-  - mx -- a matrix argument
-  - N -- ring opposite, as in `mulNr : (- x) * y = - (x * y).`
-  - V -- ring inverse, as in `mulVr : x^-1 * x = 1.`
-  - X -- ring exponentiation, as in `rmorphX : f (x ^+ n) = f x ^+ n.`
-  - Z -- (left) module scaling, as in `linearZ : f (a *: v)  = s *: f v.`
-  - z -- a int operation
+  - `T` or `t` -- boolean truth, as in `andbT: right_id true andb.`
+        -- alternatively, total set
+  - `U` -- predicate or set union, as in `predU`.
+  - `W` -- weakening, as in `in1W : {in D, forall x, P} -> forall x, P.`
+  - `0` -- ring or nat 0, or empty set, as in `addr0 : x + 0 = x.`
+  - `1` -- ring; nat or group 1, as in `mulr1 : x * 1 = x.`
+  - `D` -- addition, as in `linearD : f (u + v) = f u + f v.`
+  - `B` -- subtraction, as in `opprB : - (x - y) = y - x.`
+  - `M` -- multiplication, as in `invfM : (x * y)^-1 = x^-1 * y^-1.`
+  - `Mn` -- ring nat multiplication, as in `raddfMn : f (x *+ n) = f x *+ n.`
+  - `V` -- multiplicative inverse, as in `mulVr : x^-1 * x = 1.`
+  - `X` -- exponentiation, as in `rmorphX : f (x ^+ n) = f x ^+ n.`
+  - `Z` -- (left) module scaling, as in `linearZ : f (a *: v)  = s *: f v.`
+  - `z` -- an int argument
 #### Typical search pattern
 `Search _ "prefix" "suffix"* (symbol|pattern)* in library.`