tests and fixes

GNUmakefile

+tests:
+	lambdapi prelude/core/prelude.lp

prelude/cert_f/booleans.lp

-require open encodings.cf
+require open encodings.cert_f
 
 definition bool ≔ Prop
 definition false ≔ @prod Type Prop uProp (λ x : Term uProp, x)
 definition true ≔ Term false ⇒ Term false
 
-definition bnot (P: Term uProp) ≔ @prod Prop Prop P (λ x, false)
+definition bnot (P: Term uProp) ≔ @prod Prop Prop P (λ _, false)

prelude/cert_f/equalities.lp

-require open encodings.cf prelude.cf.booleans
+require open encodings.cert_f prelude.cert_f.booleans
 
 symbol eq {T: Term uType}: Term T ⇒ Term T ⇒ Term uProp

prelude/cert_f/int.lp

-require open encodings.cf prelude.cf.booleans prelude.cf.notequal
+require open encodings.cert_f prelude.cert_f.booleans prelude.cert_f.notequal
 
 constant symbol integer : Term uType
 definition int ≔ integer

prelude/cert_f/naturalnumbers.lp

-require open encodings.cf prelude.cf.booleans
+require open encodings.cert_f prelude.cert_f.booleans
 
 constant symbol nat : Term uType
 constant symbol zero : Term nat

prelude/cert_f/notequal.lp

-require open encodings.cf prelude.cf.booleans prelude.cf.equalities
+require open encodings.cert_f prelude.cert_f.booleans prelude.cert_f.equalities
 
 definition neq {T: Term uType} (x y: Term T) ≔ bnot (eq x y)

prelude/core/prelude.lp

-require open pvs_core prelude.booleans prelude.equalities prelude.notequal
-require open prelude.if_def
+require encodings.pvs_core prelude.core.booleans prelude.core.equalities
+prelude.core.notequal prelude.core.if_def