From c0b586318cfc3033915e9321ceeb52dbdf3970ff Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 15 Apr 2020 14:03:57 +0200
Subject: [PATCH] misc

---
 encodings/subtype.lp | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/encodings/subtype.lp b/encodings/subtype.lp
index b978a29..9aabd5a 100644
--- a/encodings/subtype.lp
+++ b/encodings/subtype.lp
@@ -1,6 +1,6 @@
 require open personoj.encodings.lhol
-  personoj.encodings.pvs_cert
-  personoj.encodings.booleans
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_hol
 
 set declared "↑"
 set declared "↓"
@@ -26,6 +26,8 @@ rule μ (psub {&T} _) → μ &T
 symbol μ₀: Set ⇒ Set
 rule μ₀ (psub {&T} _) → μ₀ &T
 
+compute λT: Set, μ (μ T)
+
 // Constraints
 symbol upcast {A: Set} {B: Set}: ε (A ⊑ B) ⇒ η A ⇒ η B
 definition ↑ {A} {B} ≔ upcast {A} {B}
@@ -37,11 +39,12 @@ admit
 
 symbol π {T: Set}: η (μ T) ⇒ Bool
 symbol downcast {A: Set} {B: Set} (_: ε (B ⊑ A))
-                (a: η A) (p: ε (π {A} (↑ {A} {μ A} (sub_of_sup A) a))): η B
+                (a: η A) (_: ε (π {A} (↑ {A} {μ A} (sub_of_sup A) a))): η B
 definition ↓ {A} {B} ≔ downcast {A} {B}
 
 set flag "print_implicits" on
 rule π {&T ~> &U} → λx: η &T ⇒ η (μ &U), forall (λy, π {&U} (x y))
+// rule π {psub {&T} &a} → λx: η (μ &T), π {&T} x
 rule π {psub {&T} &a}
-   → λx: η (μ &T), impd {π {&T} x} (λy, &a (↓ {μ &T} {&T} _ x y))
+   → λx: η (μ &T), (π {&T} x) ∧ (λy: ε (π {&T} x), &a (↓ {μ &T} {&T} _ x y))
 // FIXME: does not type check because μ (μ &T) is not reduced to μ &T
-- 
GitLab