renaming schemes

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

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

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