diff options
| author | Jim Fehrle | 2019-10-23 12:23:08 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-10-23 12:28:52 -0700 |
| commit | cc2e8fedc55a267d9d5a23015c173b1402e964a5 (patch) | |
| tree | ba6b508040ad181b7e712434f5653610b9806d7b /doc/sphinx/user-extensions | |
| parent | e6991dce306c41352c359a8ba5d6d9d6c5e6dfb2 (diff) | |
Better wording for "Show Proof" and fix typos
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index bcc5e914ac..a28ce600ca 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -750,12 +750,12 @@ level is otherwise given explicitly by using the syntax Levels are cumulative: a notation at level ``n`` of which the left end is a term shall use rules at level less than ``n`` to parse this -sub-term. More precisely, it shall use rules at level strictly less +subterm. More precisely, it shall use rules at level strictly less than ``n`` if the rule is declared with ``right associativity`` and rules at level less or equal than ``n`` if the rule is declared with ``left associativity``. Similarly, a notation at level ``n`` of which the right end is a term shall use by default rules at level strictly -less than ``n`` to parse this sub-term if the rule is declared left +less than ``n`` to parse this subterm if the rule is declared left associative and rules at level less or equal than ``n`` if the rule is declared right associative. This is what happens for instance in the rule |