change root_path and Makefile

Author: fblanqui

Bool.lp

@@ -1,6 +1,6 @@
 // Booleans
 
-require open Stdlib.Set Stdlib.Prop Stdlib.FOL;
+require open Blanqui.Lib.Set Blanqui.Lib.Prop Blanqui.Lib.FOL;
 
 inductive 𝔹 : TYPE ≔
 | true : 𝔹

Eq.lp

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

FOL.lp

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

List.lp

@@ -1,6 +1,6 @@
 // Polymorphic lists
 
-require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq Stdlib.Nat;
+require open Blanqui.Lib.Set Blanqui.Lib.Prop Blanqui.Lib.FOL Blanqui.Lib.Eq Blanqui.Lib.Nat;
 
 (a:Set) inductive 𝕃:TYPE ≔
 | □ : 𝕃 a // \Box

Makefile

@@ -1,10 +1,19 @@
-LP_SRC = $(wildcard *.lp)
-LP_OBJ = $(LP_SRC:%.lp=%.lpo)
+SRC = $(wildcard *.lp)
+OBJ = $(SRC:%.lp=%.lpo)
 
-default: $(LP_OBJ)
+default:
+	lambdapi check $(SRC)
 
-$(LP_OBJ)&: $(LP_SRC)
-	lambdapi check --gen-obj $^
+lpo: $(OBJ)
+
+$(OBJ)&: $(SRC)
+	lambdapi check -c $^
 
 clean:
-	rm -f $(LP_OBJ)
+	rm -f $(OBJ)
+
+install: lpo
+	lambdapi install lambdapi.pkg $(SRC) $(OBJ)
+
+uninstall:
+	lambdapi uninstall lambdapi.pkg

Nat.lp

@@ -1,6 +1,6 @@
 // Natural numbers
 
-require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq;
+require open Blanqui.Lib.Set Blanqui.Lib.Prop Blanqui.Lib.FOL Blanqui.Lib.Eq;
 
 inductive ℕ : TYPE ≔
 | zero : ℕ

NatBool.lp

@@ -1,4 +1,4 @@
-require open Stdlib.Bool Stdlib.Nat;
+require open Blanqui.Lib.Bool Blanqui.Lib.Nat;
 
 // Boolean equality on ℕ
 

lambdapi.pkg

@@ -1,2 +1,2 @@
-package_name = Stdlib
-root_path = Stdlib
+package_name = blanqui-lib
+root_path = Blanqui.Lib