Inf: remove builtins

.github/dependabot.yml

@@ -0,0 +1,7 @@
+version: 2
+
+updates:
+  - package-ecosystem: github-actions
+    directory: /
+    schedule:
+      interval: weekly

.github/workflows/main.yml

@@ -1,22 +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.0, lambdapi.2.4.1, lambdapi.2.4.0, lambdapi.2.3.1, lambdapi.2.3.0, lambdapi.2.2.1, lambdapi.2.2.0, lambdapi.2.1.0, lambdapi.2.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, lambdapi.2.3.0, lambdapi.2.2.1, lambdapi.2.2.0, lambdapi.2.1.0, lambdapi.2.0.0]
     runs-on: ubuntu-latest
     steps:
       - name: Check out library
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
       - name: Install ocaml and opam
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
-          ocaml-compiler: 4.14.0
+          ocaml-compiler: 4.14.2
+          # 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 for testing the development version

U/Inf.lp

@@ -1,15 +1,15 @@
 require open Logic.U.Set Logic.U.Prop;
 
-constant symbol zero : El ι; builtin "0" ≔ zero;
+constant symbol zero : El ι;
 
-constant symbol succ : El ι → El ι; builtin "+1" ≔ succ;
+constant symbol succ : El ι → El ι;
 
 symbol pred : El ι → El ι;
 
-rule pred 0 ↪ 0
+rule pred zero ↪ zero
 with pred (succ $x) ↪ $x;
 
 symbol positive : El ι → Prop;
 
-rule positive 0 ↪ ⊥
+rule positive zero ↪ ⊥
 with positive (succ _) ↪ ⊤;