diff options
| author | Cyril Cohen | 2017-12-11 11:05:31 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2017-12-11 11:05:31 +0100 |
| commit | 7e9df26ca2a95b465244d3102f11f465f27f3aea (patch) | |
| tree | 3d4c9282f9079596a1506c12829d26e85923b664 | |
| parent | 6b25220e33cd141a3fc219e31f7251c0ee47fae7 (diff) | |
fixing typos
| -rw-r--r-- | CONTRIBUTING.md | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 02b4431..e856d65 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -59,7 +59,7 @@ We write ## Statements of lemmas, theorems and definitions. -- Universal quantifications with dependent variable should appear on the left hand side of the colon, until we reach the first non dependent variable. e.g. +- Universal quantifications with dependent variable should appear on the left hand side of the colon, until we reach the first non dependent variables. e.g. `Lemma example x y : x < y -> x >= y = false` ### Term style. @@ -71,8 +71,8 @@ This particular example can be problematic if matrix.v is imported because then, + Hypothesis should not be named `H`, `H'`,... (these collide with subgroup variable conventions) but have meaningful names. For example, an hypothesis `n > 0` should be named `n_gt0`. - + Induction Hypothesies are prefixed by `IH` or `ih` (e.g. induction hypothesis on `n` is called `IH`). - + Natural numbers and integers should be names `m`, `n`, `p`, `d`, ... + + Induction Hypotheses are prefixed by `IH` or `ih` (e.g. induction hypothesis on `n` is called `IH`). + + Natural numbers and integers should be named `m`, `n`, `p`, `d`, ... + Elements of another ring should be named `x`, `y`, `z`, `u`, `v`, `w`, ... - + Polynomials are named by lower case letter `p`, `q`, `r` ... (to avoid collision with properties named `P`, `Q`, ...) - + Matrices are named `M`, `N`, `D`, ... + + 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`, ... |