From 38bf92b657fca8f7d4d72cbcdcae6fe5fed41340 Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Sat, 5 Dec 2020 09:34:05 +0100
Subject: [PATCH] Comments, renaming

---
 encodings/equality_tup.lp       | 3 +++
 encodings/{dtuple.lp => sum.lp} | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)
 rename encodings/{dtuple.lp => sum.lp} (94%)

diff --git a/encodings/equality_tup.lp b/encodings/equality_tup.lp
index 47f10fc..fa57326 100644
--- a/encodings/equality_tup.lp
+++ b/encodings/equality_tup.lp
@@ -1,7 +1,10 @@
+// Equality defined on tuple of arguments
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require personoj.encodings.tuple as T
 require open personoj.encodings.logical
 
+// Equality operates on the maximal supertype. It allows to profit
+// from predicate subtyping for free in the propositional equality.
 symbol eq {t: Set} (_: El (T.t (μ t) (μ t))): Bool
 definition neq {t} m ≔ ¬ (@eq t m)
diff --git a/encodings/dtuple.lp b/encodings/sum.lp
similarity index 94%
rename from encodings/dtuple.lp
rename to encodings/sum.lp
index 1e4e9c1..a0b9357 100644
--- a/encodings/dtuple.lp
+++ b/encodings/sum.lp
@@ -1,4 +1,4 @@
-// Dependent tuples
+// Dependent sum type
 require open personoj.encodings.lhol
 
 constant symbol t (a: Set): (El a → Set) → Set
-- 
GitLab