From c66e282477d23e3d5df80adaf8b49c14b6d5d682 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 3 Jun 2020 13:26:38 +0200
Subject: [PATCH] documentation

---
 README.md            | 22 +++++++++++++++-------
 encodings/deptype.lp |  2 ++
 encodings/lhol.lp    |  2 +-
 encodings/prenex.lp  | 16 +++++++++++-----
 4 files changed, 29 insertions(+), 13 deletions(-)

diff --git a/README.md b/README.md
index ac05d9b..6dec03f 100644
--- a/README.md
+++ b/README.md
@@ -13,14 +13,22 @@ library, also known as _Prelude_. The prelude is available
 
 
 ## Requirements
+
 [`lambdapi`](https://github.com/Deducteam/lambdapi.git) later than 
 fda8752584af52cdc8158a7a80bbe7fce5720616
 
 ## Structure
-- `adlib` contains additional libraries not in the prelude
-- `encodings` contains encodings of PVS into Dedukti, most of the work is done
-  using `cert_f` encoding
-- `prelude` contains parts of the PVS prelude
-- `sandbox` contains miscellaneous experiments
-- `tools` contains some additional scripts and utilities
-- `alternatives` contains files in other encodings
+
+- `adlib`: additional libraries not in the prelude
+- `encodings`: encoding of PVS into Dedukti
+- `prelude`: parts of the PVS prelude
+- `sandbox`: miscellaneous experiments
+- `tools`: some additional scripts and utilities
+
+## Dedukti coding conventions
+
+- Dedukti types are capitalised  
+  `Nat: TYPE`
+- Predicates are suffixed with `_p`  
+  `even_p: Nat → Bool`
+- Documentation is commented with `///`
diff --git a/encodings/deptype.lp b/encodings/deptype.lp
index 60b1624..cb2e340 100644
--- a/encodings/deptype.lp
+++ b/encodings/deptype.lp
@@ -1,8 +1,10 @@
 /// Dependent types
+
 /// PVS allows dependent types using theory abstraction. For instance,
 /// vector[t: TYPE, n: nat]: THEORY BEGIN vec: TYPE END vector
 /// allows to define
 /// cons(n: nat, e: t, v: vector[t, n].vec): vector[t, n + 1].vec
+
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 0fc57f8..7418cef 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -1,4 +1,4 @@
-// Encoding of λHOL
+/// Encoding of λHOL
 symbol Kind: TYPE
 symbol Set: TYPE
 symbol Bool: TYPE
diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index e2b4901..4bd990b 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -1,4 +1,10 @@
-// Prenex polymorphism: prenex quantification on elements of type ‘Set’.
+/// Prenex polymorphism
+
+/// Prenex polymorphism allows to quantify over variables of type ‘Set’.
+/// PVS allows it in theory formals, such as
+/// groups[t: TYPE]: THEORY BEGIN ... END groups
+/// For more informations on the encoding of prenex polymorphism, see
+/// https://arxiv.org/abs/1807.01873 and theory U
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
@@ -11,17 +17,17 @@ set declared "∀S"
 // Quantification for objects of type ‘Bool’
 set declared "∀B"
 
-symbol SchemeK: TYPE
+constant symbol SchemeK: TYPE
 symbol ϕ: SchemeK → TYPE
-symbol scheme_k: Kind → SchemeK
+constant symbol scheme_k: Kind → SchemeK
 rule ϕ (scheme_k $X) ↪ θ $X
 
 constant symbol ∀K: (Set → SchemeK) → SchemeK
 rule ϕ (∀K $e) ↪ Πt: Set, ϕ ($e t)
 
-symbol SchemeS: TYPE
+constant symbol SchemeS: TYPE
 symbol χ: SchemeS → TYPE
-symbol scheme_s: Set → SchemeS
+constant symbol scheme_s: Set → SchemeS
 rule χ (scheme_s $X) ↪ η $X
 
 constant symbol ∀S: (Set → SchemeS) → SchemeS
-- 
GitLab