From 3223066d349e37d4ac57a0b7e2f7a125fdf06044 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 30 Oct 2024 10:10:31 +0900 Subject: [PATCH] Doc: clarify ac canonical forms (#1147) --- doc/commands.rst | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/doc/commands.rst b/doc/commands.rst index 38b7d95a5..1d1e33c0f 100644 --- a/doc/commands.rst +++ b/doc/commands.rst @@ -128,14 +128,14 @@ the system with additional information on its properties and behavior. for every canonical term of the form ``f t u``, we have ``t ≤ u``, where ``≤`` is a total ordering on terms left unspecified. - If a symbol ``f`` is ``associative left`` then there is no - canonical term of the form ``f t (f u v)`` and thus every - canonical term headed by ``f`` is of the form ``f … (f (f t₁ t₂) - t₃) … tₙ``. If a symbol ``f`` is ``associative`` or ``associative - right`` then there is no canonical term of the form ``f (f t u) - v`` and thus every canonical term headed by ``f`` is of the form - ``f t₁ (f t₂ (f t₃ … tₙ) … )``. Moreover, in both cases, if ``f`` - is also ``commutative`` then we have ``t₁ ≤ t₂ ≤ … ≤ tₙ``. + If a symbol ``f`` is ``commutative`` and ``associative left`` then + there is no canonical term of the form ``f t (f u v)`` and thus + every canonical term headed by ``f`` is of the form ``f … (f (f t₁ + t₂) t₃) … tₙ``. If a symbol ``f`` is ``commutative`` and + ``associative`` or ``associative right`` then there is no + canonical term of the form ``f (f t u) v`` and thus every + canonical term headed by ``f`` is of the form ``f t₁ (f t₂ (f t₃ … + tₙ) … )``. Moreover, in both cases, we have ``t₁ ≤ t₂ ≤ … ≤ tₙ``. - **Exposition modifiers** define how a symbol can be used outside the module where it is defined. By default, the symbol can be used