quoting terms

encodings/lazy.lp

@@ -5,12 +5,15 @@ require open
 constant symbol delayed: Set ⇒ TYPE
 constant symbol quote {T: Set}: η T ⇒ delayed T
 
-constant symbol s_app: Set ⇒ Set ⇒ Set
+// Application at sort type
+symbol sapp: Set ⇒ Set ⇒ Set
+rule sapp (&T ~> &S) &T → &T
 
+// Quoted terms application
 constant symbol app {T: Set} {S: Set}
-: delayed T ⇒ delayed S ⇒ delayed (s_app T S)
+: delayed T ⇒ delayed S ⇒ delayed (sapp T S)
 
+// Unquote terms
 symbol unquote {T: Set}: delayed T ⇒ η T
-
 rule unquote (quote &x) → &x
 rule unquote {&S} (app {&T ~> &S} {&T} &t &u) → (unquote &t) (unquote &u)

sandbox/quote.lp

+require open
+  personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+require personoj.encodings.lazy as L
+
+symbol T: Set
+symbol t: η T
+symbol f: η (T ~> T)
+symbol S: Set
+symbol s: η S
+
+set flag "print_implicits" on
+definition qu_ko ≔ L.app (L.quote f) (L.quote s)
+compute L.unquote qu_ko
+
+definition qu_ok ≔ L.app (L.quote f) (L.quote t)
+compute L.unquote qu_ok