Adapt to lambdapi PR1182 + some renamings and fixes (#29)

- Z: rename × into *, and ~ into —
- Z: add parsing from decimal notation
- Nat: rename 0 into _0, and -1 into ∸1
- Z: fix missing notation for ≥
- Pos, Z: add printing to decimal notation

Author: fblanqui

.github/workflows/main.yml

@@ -1,23 +1,23 @@
 on:
   pull_request:
-    types: [opened, synchronize, edited, reopened]
+    types: [opened, synchronize, reopened]
   push:
   workflow_dispatch:
 jobs:
   build:
     strategy:
       fail-fast: false
       matrix:
-        lambdapi-version: [lambdapi,lambdapi.2.5.1,lambdapi.2.5.0,lambdapi.2.4.1,lambdapi.2.4.0,lambdapi.2.3.1,lambdapi.2.3.0]
-        # lambdapi.2.3.0 dependencies require ocaml < 5.0.0
+        lambdapi-version: [lambdapi] #,lambdapi.2.5.1,lambdapi.2.5.0,lambdapi.2.4.1,lambdapi.2.4.0,lambdapi.2.3.1]
     runs-on: ubuntu-latest
     steps:
       - name: Check out library
         uses: actions/checkout@v4
       - name: Install ocaml and opam
         uses: ocaml/setup-ocaml@v3
         with:
-          ocaml-compiler: 4.14.1
+          ocaml-compiler: 5.2.1
+          # lambdapi.2.3.0 dependencies require ocaml < 5.0.0
       - name: Install required libraries
         run: sudo apt-get install -y libev-dev
       - name: Setup opam (when testing the development version of lambdapi)

CHANGES.md

@@ -5,15 +5,26 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ## Unreleased
 
+### Added
+
+- HOL: Set constructor ⤳ for quantifying over function types
+- Impred: Set constructor o for quantifying over propositions
+- Epsilon: Hilbert's ε operator
 - List: add iota and indexes
-- Bool: declare istrue as a coercion
-- Add files for higher-order logic:
-  HOL: Set constructor ⤳ for quantifying over function types
-  Impred: Set constructor o for quantifying over propositions
-  Epsilon: Hilbert's ε operator
 - Set: add ι:Set
+- Pos, Z: add printing to decimal notation
+
+### Changed
+
+- Z: rename × into *, and ~ into —
+- Z: add parsing from decimal notation
+- Nat: rename 0 into _0, and -1 into ∸1
 - Bool: declare istrue as injective
 
+### Fixed
+
+- Z: missing notation for ≥
+
 ## 1.1.0 (2024-06-21)
 
 - Classic: classical logic

List.lp

@@ -309,7 +309,7 @@ end;
 
 symbol nilp [a] l ≔ is0 (@size a l);
 
-opaque symbol size_behead [a] (l:𝕃 a) : π (size (behead l) = size l -1) ≔
+opaque symbol size_behead [a] (l:𝕃 a) : π (size (behead l) = size l ∸1) ≔
 begin
   assume a; induction
   { reflexivity; }