ad hoc poly, equality

encodings/ad_hoc.lp

+require open personoj.encodings.lhol
+             personoj.encodings.pvs_cert
+             personoj.encodings.subtype
+             personoj.encodings.equality
+
+symbol forall_sub: Set ⇒ (Set ⇒ Set) ⇒ Set
+rule η (forall_sub &T &C) → ∀U: Set, ε (U ⊑ &T) ⇒ η (&C U)

encodings/equality.lp

+require open personoj.encodings.lhol
+
+symbol equal {T: Set}: η T ⇒ η T ⇒ Bool
+set infix left 6 "=" ≔ equal
+set builtin "T" ≔ η
+set builtin "P" ≔ ε
+set builtin "eq" ≔ equal

encodings/lhol.lp

@@ -27,3 +27,6 @@ rule ε (forall {&X} &P) → ∀x: η &X, ε (&P x)
 symbol arr: Set ⇒ Set ⇒ Set
 rule η (arr &X &Y) → (η &X) ⇒ (η &Y)
 set infix right 6 "~>" ≔ arr
+
+set builtin "T" ≔ η
+set builtin "P" ≔ ε

encodings/subtype.lp

@@ -13,6 +13,8 @@ symbol Arr (t u1 u2: Set): ε (u1 ⊑ u2) ⇒ ε ((t ~> u1) ⊑ (t ~> u2))
 symbol 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
+
 symbol root: Set ⇒ Set
 rule root (psub {&T} _) → root &T