From 4a339148152cef407b8b748181fce7722ff00c9c Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Tue, 26 May 2020 14:39:24 +0200
Subject: [PATCH] renaming schemes

---
 encodings/prenex.lp | 14 +++++++-------
 paper/equal.lp      |  2 +-
 prelude/logic.lp    |  2 +-
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index bf2e6c5..e2b4901 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -13,18 +13,18 @@ set declared "∀B"
 
 symbol SchemeK: TYPE
 symbol ϕ: SchemeK → TYPE
-symbol schemeK: Kind → SchemeK
-rule ϕ (schemeK $X) ↪ θ $X
+symbol scheme_k: Kind → SchemeK
+rule ϕ (scheme_k $X) ↪ θ $X
 
 constant symbol ∀K: (Set → SchemeK) → SchemeK
 rule ϕ (∀K $e) ↪ Πt: Set, ϕ ($e t)
 
-symbol Scheme: TYPE
-symbol χ: Scheme → TYPE
-symbol scheme: Set → Scheme
-rule χ (scheme $X) ↪ η $X
+symbol SchemeS: TYPE
+symbol χ: SchemeS → TYPE
+symbol scheme_s: Set → SchemeS
+rule χ (scheme_s $X) ↪ η $X
 
-constant symbol ∀S: (Set → Scheme) → Scheme
+constant symbol ∀S: (Set → SchemeS) → SchemeS
 rule χ (∀S $e) ↪ Πt: Set, χ ($e t)
 
 constant symbol ∀B: (Set → Bool) → Bool
diff --git a/paper/equal.lp b/paper/equal.lp
index 150cc40..d177f9f 100644
--- a/paper/equal.lp
+++ b/paper/equal.lp
@@ -2,4 +2,4 @@ require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.prenex
 
-symbol eq: χ (∀S (λT: θ {|set|}, scheme (T ~> T ~> bool)))
+symbol eq: χ (∀S (λT: θ {|set|}, scheme_s (T ~> T ~> bool)))
diff --git a/prelude/logic.lp b/prelude/logic.lp
index 4d7d541..ffcae6f 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -60,7 +60,7 @@ admit
 //
 // Defined types
 //
-definition pred: ϕ (∀K (λ_, schemeK {|set|})) ≔ λt, t ~> bool
+definition pred: ϕ (∀K (λ_, scheme_k {|set|})) ≔ λt, t ~> bool
 definition PRED ≔ pred
 definition predicate ≔ pred
 definition PREDICATE ≔ pred
-- 
GitLab