fblanqui · Oct 3, 2026 · Oct 3, 2026
diff --git a/Bool.lp b/Bool.lp
@@ -1,4 +1,4 @@
-/* Library on booleans. */
+// booleans
 
 require open Stdlib.FOL Stdlib.Eq;
 

diff --git a/Comp.lp b/Comp.lp
@@ -1,6 +1,4 @@
-/* Comparison datatype
-
-By Quentin Garchery (May 2021). */
+// comparison datatype
 
 require open Stdlib.Bool;
 

diff --git a/Conj.lp b/Conj.lp
@@ -1,7 +1,6 @@
-/* Library on Meta-Theorems for Conjunctions
-
--------------------
+// varyadic conjunction
 
+/*
 The library proves the following meta-theorems:
 
 ** n-ary Natural Deduction rules:
@@ -122,4 +121,4 @@ begin
             have ConjImpCl : π (conj cnf ⇒ clause cnf id)
                 {refine h0 cnf (indexes_decrement id x cnf h2)};
             refine clause_ext cnf x id (ConjImpCl (conj_tail x cnf h3))}}
-end;
+end;
diff --git a/Coprod.lp b/Coprod.lp
@@ -1,4 +1,4 @@
-// Co-Cartesian product (disjoint sum)
+// disjoint sum
 
 require open Stdlib.FOL Stdlib.Eq;
 

diff --git a/DepProd.lp b/DepProd.lp
@@ -1,4 +1,4 @@
-// Dependent product: a dependent pair of an element and an element in Set
+// dependent pairs
 
 require open Stdlib.Eq;
 
@@ -9,11 +9,11 @@ constant symbol dprod [a: Set] : (τ a → Set) → Set;
 
 rule τ (@dprod $a $p) ↪ @DProd $a $p;
 
-symbol proj₁ [a] [p] (e: @DProd a p) : τ a;
+symbol proj₁ [a p] (e: @DProd a p) : τ a;
 
 rule proj₁ (dpair $x _) ↪ $x;
 
-symbol proj₂ [a] [p] (e: @DProd a p) : τ (p (proj₁ e));
+symbol proj₂ [a p] (e: @DProd a p) : τ (p (proj₁ e));
 
 rule proj₂ (dpair _ $u) ↪ $u;
 
@@ -23,13 +23,11 @@ begin assume a p; induction; reflexivity end;
 
 opaque symbol eq_proj₁ [a] [p] (x y: @DProd a p) :
   π (x = y) → π (proj₁ x = proj₁ y) ≔
-begin assume a p x y h; refine feq (λ e, proj₁ e) h end;
+begin assume a p x y h; refine feq proj₁ h end;
 
 opaque symbol eq_dpair_refl [a] [p] (x: τ a) (u v: τ (p x)) :
   π (u = v) → π (@dpair a p x u = dpair x v) ≔
-begin
-  assume a p x u v h; refine feq (λ w, @dpair a p x w) h
-end;
+begin assume a p x u v h; refine feq (dpair x) h end;
 
 symbol transport [a] (p: τ a → Set) [x y: τ a] : π (x = y) → τ (p x) → τ (p y);
 rule transport _ (eq_refl _) $u ↪ $u;

diff --git a/Disj.lp b/Disj.lp
@@ -1,7 +1,6 @@
-/* Library on Meta-Theorems for Disjunctions
-
--------------------
+// varyadic disjunction
 
+/*
 The library proves the following meta-theorems:
 
 ** n-ary Natural Deduction rules:
@@ -400,4 +399,4 @@ begin
 end;
 
 assert l0 l1 l2 l2' ⊢ transform [l2'] (l0 ⸬ l1 ⸬ l2 ⸬ l1 ⸬ □) 2 :
-    (π l2 → π l2') →  π (l0 ∨ l1 ∨ l2 ∨ l1) → π (l0 ∨ l1 ∨ l2' ∨ l1);
+    (π l2 → π l2') →  π (l0 ∨ l1 ∨ l2 ∨ l1) → π (l0 ∨ l1 ∨ l2' ∨ l1);
diff --git a/Epsilon.lp b/Epsilon.lp
@@ -1,3 +1,5 @@
+// Hilbert choice operator
+
 require open Stdlib.FOL;
 
 symbol ε [a:Set] : (τ a → Prop) → τ a;

diff --git a/ExtraRules.lp b/ExtraRules.lp
@@ -1,4 +1,4 @@
-// This module turns proved equalities to rewrite rules
+// additional rewrite rules derived from proved equalities
 
 // Bool
 

diff --git a/FOL.lp b/FOL.lp
@@ -1,4 +1,4 @@
-// (multi-sorted) First-order logic
+// polymorphic first-order logic
 
 require open Stdlib.Set Stdlib.Prop;
 

diff --git a/HOL.lp b/HOL.lp
@@ -1,3 +1,5 @@
+// higher-order logic
+
 require open Stdlib.Set;
 
 constant symbol ⤳ : Set → Set → Set; // \leadsto

diff --git a/Impred.lp b/Impred.lp
@@ -1,3 +1,5 @@
+// impredicativity (quantification on propositions)
+
 require open Stdlib.Set Stdlib.Prop;
 
 symbol o : Set;

diff --git a/List.lp b/List.lp
@@ -1,5 +1,6 @@
-/* Library on polymorphic lists
+// polymorphic lists
 
+/*
 following https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/seq.v
 
 seq.v documentation

diff --git a/NaryFun.lp b/NaryFun.lp
@@ -1,5 +1,6 @@
-/* n-ary functions and relations
+// n-ary functions and relations
 
+/*
 following "Generic Level Polymorphic N-ary Functions" by Guillaume
 Allais (TyDe 2019). */
 

diff --git a/Nat.lp b/Nat.lp
@@ -1,5 +1,6 @@
-/* Library on natural numbers
+// unary natural numbers
 
+/*
 following https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnat.v
 
 Documentation of ssrnat.v

diff --git a/Pos.lp b/Pos.lp
@@ -1,5 +1,6 @@
-// Positive binary integers following Rocq stdlib
+// positive binary integers
 
+//  following Rocq stdlib
 require open Stdlib.Nat Stdlib.Comp;
 
 inductive ℙ : TYPE ≔

diff --git a/Prod.lp b/Prod.lp
@@ -58,7 +58,7 @@ begin reflexivity end;
 
 symbol prodExt [a b] (x: τ (a × b)) : π (x = (x ₁) ‚ (x ₂)) ≔
 begin
-  assume a; refine ind_Prod a (λ b x, x = (x ₁) ‚ (x ₂)) _; reflexivity
+  assume a b; refine ind_Prod (λ x, x = (x ₁) ‚ (x ₂)) _; reflexivity
 end;
 
 opaque symbol eq_pair [a b] (x y: τ (a × b)) :

diff --git a/Prop.lp b/Prop.lp
@@ -1,4 +1,4 @@
-// Propositional logic
+// propositional logic
 
 constant symbol Prop : TYPE;
 

diff --git a/PropExt.lp b/PropExt.lp
@@ -1,3 +1,5 @@
+// propositional extensionality
+
 /***************************************************************************
 This file provides an axiom and various theorems for propositional equality.
 The theorems are grouped into sections by theme:

diff --git a/Quotient.lp b/Quotient.lp
@@ -1,4 +1,4 @@
-// Quotient types
+// quotient types
 
 require open Stdlib.Eq;
 
@@ -12,7 +12,6 @@ notation ⫽ infix 30;
 rule τ (_ ⫽ $R) ↪ Quot $R;
 
 symbol class [a] r ≔ @cl a r;
-symbol ind_quot [a] ≔ ind_Quot a;
 
 symbol sound [a] (r:Rel a) x y: π(r x y) → π (class r x = class r y);
 
@@ -31,7 +30,7 @@ begin
     { assume x x' xx'; set p ≔ λ x y y' yy', hf x x (hr x) y y' yy';
       change π(lift r (f x) (p x) d = lift r (f x') (p x') d);
       set q ≔ λ d, lift r (f x) (p x) d = lift r (f x') (p x') d;
-      change π(q d); apply ind_quot r q _ d;
+      change π(q d); apply ind_Quot q _ d;
       assume y; simplify; apply hf {apply xx'} {apply hr} }
 end;
 

diff --git a/QuotientExample.lp b/QuotientExample.lp
@@ -1,4 +1,4 @@
-// example of quotient: integers
+// example of quotient type
 
 require open Stdlib.Nat Stdlib.Prod Stdlib.Quotient;
 
@@ -38,7 +38,7 @@ require open Stdlib.FOL;
 
 opaque symbol +_com a b: π (+ a b = + b a) ≔
 begin
-  refine ind_quot intrel (λ a, `∀ b, + a b = + b a) _; assume x;
-  refine ind_quot intrel (λ b, + (class intrel x) b = + b (class intrel x)) _; assume y;
+  refine ind_Quot (λ a, `∀ b, + a b = + b a) _; assume x;
+  refine ind_Quot (λ b, + (class intrel x) b = + b (class intrel x)) _; assume y;
   apply sound; simplify; rewrite addnC (x ₁); rewrite addnC (y ₂); reflexivity
 end;
diff --git a/README.md b/README.md
@@ -1,36 +1,54 @@
 Standard library of [Lambdapi](https://github.com/Deducteam/lambdapi)
 =====================================================================
 
-- `Prop`: propositional logic
-- `Eq`: equality
-- `Set`: set codes for polymorphism
-- `FOL`: typed first-order logic
 - `Bool`: booleans
-- `Nat`: natural numbers
-- `List`: polymorphic lists
 - `Classic`: classical logic
+- `Comp`: comparison datatype
+- `Conj`: varyadic conjunction
+- `Coprod`: disjoint sum
+- `DepProd`: dependent pairs
+- `Disj`: varyadic disjunction
+- `Epsilon`: Hilbert choice operator
+- `Eq`: polymorphic Leibniz equality
+- `ExtraRules`: additional rewrite rules derived from proved equalities
+- `FOL`: polymorphic first-order logic
+- `FunExt`: require open Stdlib.Eq Stdlib.HOL;
+- `HOL`: higher-order logic
+- `Impred`: impredicativity (quantification on propositions)
+- `List`: polymorphic lists
+- `NaryFun`: n-ary functions and relations
+- `Nat`: unary natural numbers
+- `Option`: option type
+- `Pos`: positive binary integers
+- `Prod`: Cartesian product
+- `PropExt`: propositional extensionality
+- `Prop`: propositional logic
+- `QuotientExample`: example of quotient type
+- `Quotient`: quotient types
+- `Set`: type of type codes
+- `String`: builtin string type
+- `Subset`: subset types
+- `Tactic`: tactic type
+- `Univ`: universes
+- `Z`: binary integers
 
 The libraries on natural numbers and polymorphic lists follow the
-corresponding Coq SSReflect libraries:
-
-- [ssrnat.v](https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnat.v)
-
-- [seq.v](https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/seq.v)
+corresponding Rocq SSReflect libraries [ssrnat.v](https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnat.v)
+and [seq.v](https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/seq.v). The library on integers follow the one of the Rocq standard library.
 
 Installation with Opam
 ----------------------
 
 ```
-opam repository -a --set-default add lambdapi https://github.com/deducteam/opam-lambdapi-repos
-itory.git # once
+opam repository -a --set-default add lambdapi https://github.com/deducteam/opam-lambdapi-repository.git # once
 opam install lambdapi-stdlib
 ```
 
 Usage in Lambdapi
 -----------------
 
 ```
-require open Stdlib.Prop Stdlib.Set Stdlib.FOL Stdlib.Nat /* ... */;
+require open Stdlib.Nat;
 ```
 
 Compilation from the sources

diff --git a/Set.lp b/Set.lp
@@ -1,4 +1,4 @@
-// Type of set codes for quantifying over sets (polymorphism)
+// type of type codes
 
 constant symbol Set : TYPE;
 

diff --git a/String.lp b/String.lp
@@ -1,4 +1,4 @@
-// builtin type of strings
+// builtin string type
 
 require open Stdlib.Set;
 

diff --git a/Subset.lp b/Subset.lp
@@ -1,4 +1,4 @@
-// Subset types: a dependent pair of an element and a proof
+// subset types
 
 require open Stdlib.FOL Stdlib.Eq;
 

diff --git a/Tactic.lp b/Tactic.lp
@@ -1,4 +1,4 @@
-// define a type representing Lambdapi tactics
+// tactic type
 
 require open Stdlib.String Stdlib.Univ;
 

diff --git a/Univ.lp b/Univ.lp
@@ -1,3 +1,5 @@
+// universes
+
 require open Stdlib.Set Stdlib.Prop;
 
 constant symbol L:TYPE;

diff --git a/Z.lp b/Z.lp
@@ -1,5 +1,6 @@
-// Binary integers (following Rocq stdlib)
+// binary integers
 
+// following Rocq stdlib
 require open Stdlib.Pos;
 
 inductive ℤ : TYPE ≔ // \BbbZ

diff --git a/summary b/summary
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+for f in `ls *.lp`
+do
+    echo "- \`${f%.lp}\`: `head -n1 $f | sed -e 's/^\/\/ //'`"
+done