Deducteam · fblanqui · Feb 27, 2023 · Feb 27, 2023 · Feb 27, 2023
diff --git a/Bool.lp b/Bool.lp
@@ -1,6 +1,6 @@
 /* Library on booleans. */
 
-require open Blanqui.Lib.Set Blanqui.Lib.Prop Blanqui.Lib.FOL Blanqui.Lib.Eq;
+require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq;
 
 inductive 𝔹 : TYPE ≔ // `dB or \BbbB
 | true : 𝔹

diff --git a/Comp.lp b/Comp.lp
@@ -2,8 +2,8 @@
 
 By Quentin Garchery (May 2021). */
 
-require open Blanqui.Lib.Set Blanqui.Lib.Prop Blanqui.Lib.FOL Blanqui.Lib.Eq
-  Blanqui.Lib.Bool;
+require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq
+  Stdlib.Bool;
 
 inductive Comp : TYPE ≔
 | Eq : Comp

diff --git a/Eq.lp b/Eq.lp
@@ -1,6 +1,6 @@
 // polymorphic Leibniz equality
 
-require open Blanqui.Lib.Set Blanqui.Lib.Prop;
+require open Stdlib.Set Stdlib.Prop;
 
 constant symbol = [a] : τ a → τ a → Prop;
 

diff --git a/FOL.lp b/FOL.lp
@@ -1,6 +1,6 @@
 // (multi-sorted) First-order logic
 
-require open Blanqui.Lib.Set Blanqui.Lib.Prop;
+require open Stdlib.Set Stdlib.Prop;
 
 // Universal quantification
 

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

diff --git a/Nat.lp b/Nat.lp
@@ -88,8 +88,8 @@ expnMn : (m1 * m2) ^ n = ... The operands of other operators are selected
 using the l/r suffixes.
 */
 
-require open Blanqui.Lib.Set Blanqui.Lib.Prop Blanqui.Lib.FOL Blanqui.Lib.Eq
-  Blanqui.Lib.Bool;
+require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq
+  Stdlib.Bool;
 
 inductive ℕ : TYPE ≔
 | 0 : ℕ

diff --git a/Pos.lp b/Pos.lp
@@ -2,8 +2,8 @@
 
 by Quentin Garchery (May 2021). */
 
-require open Blanqui.Lib.Set Blanqui.Lib.Prop Blanqui.Lib.FOL Blanqui.Lib.Eq
-  Blanqui.Lib.Nat Blanqui.Lib.Bool Blanqui.Lib.Comp;
+require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq
+  Stdlib.Nat Stdlib.Bool Stdlib.Comp;
 
 inductive ℙ : TYPE ≔
 | I : ℙ → ℙ

diff --git a/Z.lp b/Z.lp
@@ -2,8 +2,8 @@
 
 by Quentin Garchery (May 2021). */
 
-require open Blanqui.Lib.Set Blanqui.Lib.Prop Blanqui.Lib.FOL Blanqui.Lib.Eq
-  Blanqui.Lib.Pos Blanqui.Lib.Bool;
+require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq
+  Stdlib.Pos Stdlib.Bool;
 
 inductive ℤ : TYPE ≔ // \BbbZ
 | Z0 : ℤ
@@ -349,7 +349,7 @@ end;
 
 // Comparison of integers
 
-require open Blanqui.Lib.Comp;
+require open Stdlib.Comp;
 
 symbol ≐ : ℤ → ℤ → Comp; notation ≐ infix 12; // \doteq
 

diff --git a/blanqui-lib.opam b/blanqui-lib.opam
diff --git a/lambdapi-stdlib.opam b/lambdapi-stdlib.opam
@@ -0,0 +1,28 @@
+opam-version: "2.0"
+synopsis: "Lambdapi library on natural numbers, integers and polymorphic lists"
+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
+"""
+maintainer: ["[email protected]"]
+authors: ["Frédéric Blanqui" "Quentin Buzet" "Quentin Garchery"]
+license: "CECILL-2.1"
+homepage: "https://github.com/Deducteam/lambdapi-stdlib"
+bug-reports: "https://github.com/Deducteam/lambdapi-stdlib/issues"
+dev-repo: "git+https://github.com/Deducteam/lambdapi-stdlib.git"
+install: [ make "install" ]
+uninstall: [ make "uninstall" ]
+depends: [
+  "lambdapi" {>= "2.3.0"}
+]
diff --git a/lambdapi.pkg b/lambdapi.pkg
@@ -1,2 +1,2 @@
-package_name = blanqui-lib
-root_path = Blanqui.Lib
+package_name = stdlib
+root_path = Stdlib