booleans

adlib/booleans.lp

 require open
   personoj.encodings.lhol
   personoj.encodings.pvs_cert
+  personoj.encodings.booleans
 
 definition false ≔ forall {bool} (λx, x)
 definition true ≔ impd {false} (λ_, false)
@@ -19,8 +20,6 @@ set infix 7 "⇔" ≔ biff
 
 definition when P Q ≔ imp Q P
 
-set builtin "bot" ≔ false
-set builtin "top" ≔ true
 set builtin "imp" ≔ imp
 set builtin "not" ≔ bnot
 set builtin "and" ≔ band

encodings/booleans.lp

+require open personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+
+definition false ≔ forall {bool} (λx, x)
+definition true ≔ impd {false} (λ_, false)
+
+set builtin "bot" ≔ false
+set builtin "top" ≔ true

encodings/if.lp

 require open personoj.encodings.lhol
   personoj.encodings.pvs_cert
-  personoj.encodings.subtype
+  personoj.encodings.booleans
+require personoj.encodings.deferred as Deferred
+require open personoj.encodings.subtype //FIXME: why must it be the last import?
 
 symbol if {U: Set} {V: Set} (S: Set)
 : ε (U ⊑ S) ⇒ ε (V ⊑ S) ⇒ Bool ⇒ η U ⇒ η V ⇒ η S
+
+symbol lif {U: Set} {V: Set} (S: Set)
+: ε (U ⊑ S) ⇒ ε (V ⊑ S) ⇒ Bool ⇒ Deferred.t U ⇒ Deferred.t V ⇒ η S
+
+// lazy if
+rule lif _ &pr _ true &t _ → ↑ &pr (Deferred.unquote &t)
+rule lif _ _ &pr false _ &f → ↑ &pr (Deferred.unquote &f)

encodings/subtype.lp

 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
+set declared "↑"
+
 symbol subtype : Set ⇒ Set ⇒ Bool
 set infix left 6 "⊑" ≔ subtype
 
@@ -14,6 +16,7 @@ symbol S_Darr (d: Set) (r1: η d ⇒ Set) (r2: η d ⇒ Set)
 : ε (forall (λx, (r1 x) ⊑ (r2 x))) ⇒ ε ((arrd r1) ⊑ (arrd r2))
 
 symbol upcast {A: Set} {B: Set}: ε (A ⊑ B) ⇒ η A ⇒ η B
+definition ↑ {A} {B} ≔ upcast {A} {B}
 
 symbol root: Set ⇒ Set
 rule root (psub {&T} _) → root &T

sandbox/quote.lp

@@ -17,3 +17,5 @@ definition qu_ok ≔ Deferred.app (Deferred.quote f) (Deferred.quote t)
 compute Deferred.unquote qu_ok
 
 compute Deferred.quote {T ~> T} (λx:η T, f x)
+
+symbol lor: Deferred.t bool ⇒ Deferred.t bool ⇒ Bool