From 954d9a131971576f29f764d0922a9d1f0b775c88 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 30 Oct 2024 10:10:05 +0900 Subject: [PATCH 1/2] ci: test ocaml 4.14.2 instead of 4.14.1 (#1146) --- .github/workflows/main.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index cb9075934..d5d2e1a01 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -8,7 +8,7 @@ jobs: strategy: fail-fast: false matrix: - ocaml-version: [5.2.0, 5.1.1, 5.0.0, 4.14.1, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1] + ocaml-version: [5.2.0, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1] runs-on: ubuntu-latest steps: - name: checking out lambdapi repo ... 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 2/2] 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