diff options
| -rw-r--r-- | CONTRIBUTING.md | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index ea5d631..19ab0e5 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -126,7 +126,7 @@ Abbreviations are in the header of the file which introduces them. We list here -- alternatively predicate or set intersection, as in `predI.` - `l` -- the left-hand of an operation, as in + `andb_orl : left_distributive andb orb.` - + `ltr_norml x y : (`|x| < y) = (- y < x < y).` + + ``ltr_norml x y : (`|x| < y) = (- y < x < y).`` - `L` -- the left-hand of a relation, as in `ltn_subrL : n - m < n = (0 < m) && (0 < n).` - `LR` -- moving an operator from the left-hand to the right-hand of an relation, as in `leq_subLR : (m - n <= p) = (m <= n + p).` - `N` or `n` -- boolean negation, as in `andbN : a && (~~ a) = false.` @@ -136,7 +136,7 @@ Abbreviations are in the header of the file which introduces them. We list here `andP : reflect (a /\ b) (a && b)`. - `r` -- a right-hand operation, as in + `orb_andr : right_distributive orb andb.` - + `ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y).` + + ``ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y).`` + alternatively, it is a ring argument. - `R` -- the right-hand of a relation, as in `ltn_subrR : n < n - m = false`. - `RL` -- moving an operator from the right-hand to the left-hand of an relation, as in `ltn_subRL : (n < p - m) = (m + n < p).` |