add summary script (#78)

- update following Deducteam/lambdapi#1527
- add summary script generating a one-line description of each module form its first line

Author: fblanqui

Bool.lp

@@ -1,4 +1,4 @@
-/* Library on booleans. */
+// booleans
 
 require open Stdlib.FOL Stdlib.Eq;
 

Comp.lp

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

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;

Coprod.lp

@@ -1,4 +1,4 @@
-// Co-Cartesian product (disjoint sum)
+// disjoint sum
 
 require open Stdlib.FOL Stdlib.Eq;
 

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;

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);

Epsilon.lp

@@ -1,3 +1,5 @@
+// Hilbert choice operator
+
 require open Stdlib.FOL;
 
 symbol ε [a:Set] : (τ a → Prop) → τ a;

ExtraRules.lp

@@ -1,4 +1,4 @@
-// This module turns proved equalities to rewrite rules
+// additional rewrite rules derived from proved equalities
 
 // Bool
 

FOL.lp

@@ -1,4 +1,4 @@
-// (multi-sorted) First-order logic
+// polymorphic first-order logic
 
 require open Stdlib.Set Stdlib.Prop;
 

HOL.lp

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