simplify requires (now recursive)

.github/workflows/main.yml

@@ -8,15 +8,15 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        lambdapi-version: [lambdapi,lambdapi.2.6.0] #,lambdapi.2.5.1,lambdapi.2.5.0,lambdapi.2.4.1,lambdapi.2.4.0,lambdapi.2.3.1]
+        lambdapi-version: [lambdapi,lambdapi.3.0.0] #lambdapi.2.6.0,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: 5.2.1
+          ocaml-compiler: 5.3.0
           # lambdapi.2.3.0 dependencies require ocaml < 5.0.0
       - name: Install required libraries
         run: sudo apt-get install -y libev-dev

Bool.lp

@@ -1,6 +1,6 @@
 /* Library on booleans. */
 
-require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq;
+require open Stdlib.FOL Stdlib.Eq;
 
 inductive 𝔹 : TYPE ≔ // `dB or \BbbB
 | true : 𝔹

CHANGES.md

@@ -3,7 +3,7 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
-## Unreleased
+## 1.3.0
 
 ### Added
 

Classic.lp

@@ -1,6 +1,6 @@
 // classical logic
 
-require open Stdlib.Set Stdlib.Prop Stdlib.FOL;
+require open Stdlib.FOL;
 
 symbol em p : π (p ∨ ¬ p); // excluded middle
 

Comp.lp

@@ -2,8 +2,7 @@
 
 By Quentin Garchery (May 2021). */
 
-require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq
-  Stdlib.Bool;
+require open Stdlib.Bool;
 
 inductive Comp : TYPE ≔
 | Eq : Comp

Epsilon.lp

@@ -1,4 +1,4 @@
-require open Stdlib.Set Stdlib.Prop Stdlib.FOL;
+require open Stdlib.FOL;
 
 symbol ε [a:Set] : (τ a → Prop) → τ a;
 symbol εᵢ [a:Set] (p:τ a → Prop) : π (∃ p) → π (p (ε p));

FunExt.lp

@@ -1,4 +1,3 @@
-require open Stdlib.Set Stdlib.Prop Stdlib.Eq Stdlib.FOL Stdlib.HOL;
-
-symbol funExt [a b] (f g : τ (a ⤳ b)) : π(`∀ x, f x = g x) → π(f = g);
+require open Stdlib.Eq Stdlib.HOL;
 
+symbol funExt [a b] (f g : τ (a ⤳ b)) : (Π x, π(f x = g x)) → π(f = g);

List.lp

@@ -197,8 +197,7 @@ protected with nosimpl.
  An example of use can be found in fingraph theorem orbitPcycle.
 */
 
-require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq
-  Stdlib.Nat Stdlib.Bool Stdlib.Prod;
+require open Stdlib.Nat Stdlib.Prod;
 
 (a:Set) inductive 𝕃:TYPE ≔
 | □ : 𝕃 a // \Box

Nat.lp

@@ -88,7 +88,7 @@ expnMn : (m1 * m2) ^ n = ... The operands of other operators are selected
 using the l/r suffixes.
 */
 
-require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq Stdlib.Bool;
+require open Stdlib.Bool;
 
 inductive ℕ : TYPE ≔
 | _0 : ℕ

Pos.lp

@@ -2,8 +2,7 @@
 
 by Quentin Garchery (May 2021). */
 
-require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq
-  Stdlib.Nat Stdlib.Bool Stdlib.Comp;
+require open Stdlib.Nat Stdlib.Comp;
 
 inductive ℙ : TYPE ≔
 | I : ℙ → ℙ

PropExt.lp

@@ -5,7 +5,7 @@ The theorems are grouped into sections by theme:
 - Various Simplifications                              
 ****************************************************************************/
 
-require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq Stdlib.Impred Stdlib.Classic;
+require open Stdlib.Eq Stdlib.Impred Stdlib.Classic;
 
 symbol propExt x y : (π x → π y) → (π y → π x) → π (x = y);
 

Tactic.lp

@@ -1,7 +1,6 @@
 // define a type representing Lambdapi tactics
 
-require open Stdlib.Set Stdlib.Prop Stdlib.String Stdlib.Option
-             Stdlib.List;
+require open Stdlib.String Stdlib.Option Stdlib.List;
 
 constant symbol Tactic : TYPE;
 

Z.lp

@@ -2,7 +2,7 @@
 
 by Quentin Garchery (May 2021). */
 
-require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq Stdlib.Pos Stdlib.Bool;
+require open Stdlib.Pos;
 
 inductive ℤ : TYPE ≔ // \BbbZ
 | Z0 : ℤ

lambdapi-stdlib.opam

@@ -1,19 +1,9 @@
 opam-version: "2.0"
 synopsis: "Standard library of Lambdapi"
 description: """
-This package provides a Lambdapi library on natural numbers,
-integers and polymorphic lists (in intuitionistic first-order logic).
-It provides the following modules:
-- Stdlib.Set: type of set codes
-- Stdlib.Prop: propositional logic
-- Stdlib.Eq: Leibniz equality
-- Stdlib.FOL: first-order logic
-- Stdlib.Bool: booleans
-- Stdlib.Nat: natural numbers
-- Stdlib.List: polymorphic lists
-- Stdlib.Comp: comparison result data type
-- Stdlib.Pos: binary positive numbers
-- Stdlib.Z: integers
+This Lambdapi library provides modules for defining logics, metatheorems of
+classical logic, functions and properties on basic inductive types like
+natural numbers (in base 1 and 2), integers and polymorphic lists.
 """
 maintainer: ["[email protected]"]
 authors: ["Frédéric Blanqui" "Quentin Buzet" "Quentin Garchery"]
@@ -24,5 +14,5 @@ dev-repo: "git+https://github.com/Deducteam/lambdapi-stdlib.git"
 build: [ make ]
 install: [ make "install" ]
 depends: [
-  "lambdapi" {>= "2.6.0"}
+  "lambdapi" {>= "3.0.0"}
 ]