From ec789c242216a9e2b49306bde072926b39c5dc53 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Tue, 2 Jun 2020 17:56:17 +0200
Subject: [PATCH] more prenex polymorphism

---
 encodings/prenex.lp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index e2b4901..441eeda 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -29,3 +29,10 @@ rule χ (∀S $e) ↪ Πt: Set, χ ($e t)
 
 constant symbol ∀B: (Set → Bool) → Bool
 rule ε (∀B $p) ↪ Πx: Set, ε ($p x)
+
+// Since PVS supports dependent types through theory formal parameters, we allow
+// prenex quantifications on elements “e: T” with “T: TYPE” in elements of type
+// “Kind”.
+set declared "∀k"
+constant symbol ∀k {t: Set}: (η t → SchemeK) → SchemeK
+rule ϕ (∀k {$t} $e) ↪ Πt: η $t, ϕ ($e t)
-- 
GitLab