simplify requires (now recursive) (#46)

Author: fblanqui

.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 : ℙ → ℙ