fixed implicit args of prod

adlib/cert_f/booleans.lp

 require open encodings.cert_f
 
 definition bool ≔ uProp
-definition false: Term bool ≔ @prod Type Prop uProp (λ x, x)
-definition true: Term bool ≔ @prod Prop Prop false (λ _, false)
+definition false ≔ @prod Type Prop bool (λ x, x)
+definition true ≔ @prod Prop Prop false (λ _, false)
 
-definition imp (P Q: Term uProp): Term bool ≔ @prod Prop Prop P (λ_, Q)
-definition forall {eT: Term uType} (P: Term eT ⇒ Term bool): Term bool ≔
-  @prod _ _ eT P
+definition imp (P Q: Term uProp) ≔ @prod Prop Prop P (λ_, Q)
+definition forall {T: Term uType} (P: Term T ⇒ Term bool) ≔ @prod _ _ T P
 
-definition bnot (P: Term uProp): Term bool ≔ @prod Prop Prop P (λ _, false)
+definition bnot (P: Term uProp) ≔ @prod Prop Prop P (λ _, false)
 set prefix 5 "¬" ≔ bnot
 
 definition band (P Q: Term uProp) ≔ bnot (imp P (bnot Q))
@@ -20,11 +19,10 @@ definition biff (P Q: Term bool) ≔ (imp P Q) ∧ (imp Q P)
 set infix 7 "⇔" ≔ biff
 
 definition when (P Q: Term uProp) ≔ imp Q P
-// FIXME explicitness?
 
 set builtin "bot" ≔ false
 set builtin "top" ≔ true
 set builtin "imp" ≔ imp
 set builtin "and" ≔ band
-set builtin "or" ≔ bor
+set builtin "or"  ≔ bor
 set builtin "not" ≔ bnot

encodings/cert_f.lp

@@ -28,9 +28,10 @@ rule Term uProp → Univ Prop
  and Term uType → Univ Type
 
 // [prod s1 s2 A B] encodes [Π x : (A: s1). (B: s2)]
-symbol prod {sA sB: Sort} (A: Univ sA): (Term A ⇒ Univ sB) ⇒ Univ (Rule sA sB)
+symbol prod {sA: Sort} {sB: Sort} (A: Univ sA):
+  (Term A ⇒ Univ sB) ⇒ Univ (Rule sA sB)
 
-rule Term (@prod &sA &sB &A &B) → ∀ x : Term {&sA} &A, Term {&sB} (&B x)
+rule Term (prod {&sA} {&sB} &A &B) → ∀ x : Term {&sA} &A, Term {&sB} (&B x)
 
 // Predicate subtyping
 // can be seen as a dependant pair type with
@@ -46,7 +47,7 @@ symbol fst {T: Univ Type} (P: Term T ⇒ Univ Prop): Term (Psub T P) ⇒ Term T
 //  Γ ⊢ M : { v : T | P }
 // ——————————————————————————PROJr
 // Γ ⊢ snd(M) : P[v ≔ fst(M)]
-constant symbol snd {T: Univ Type} (P: Term T ⇒ Univ Prop)
+constant symbol snd {T: Univ Type} {P: Term T ⇒ Univ Prop}
   (M: Term (Psub T P)):
   Term (P (fst P M))
 

prelude/cert_f/logic.lp

@@ -12,10 +12,11 @@ require adlib.cert_f.subtype as S
 //
 symbol eq {T: Term uType}: Term T ⇒ Term T ⇒ Term uProp
 set infix 5 "=" ≔ eq
+// set builtin "eq" ≔ eq
 
 // NOTE not in the prelude
-constant symbol cast_trans (A B C: Term uType) (prab: Term (A ⊑ B)) (prbc: Term (B ⊑ C))
-  (x: Term A):
+constant symbol cast_trans (A B C: Term uType) (prab: Term (A ⊑ B))
+  (prbc: Term (B ⊑ C)) (x: Term A):
   Term (eq (↑ {B} C prbc (↑ {A} B prab x))
   (↑ {A} C (S.trans A B C prab prbc) x))
 
@@ -80,7 +81,7 @@ definition ∃ {eT: Term uType} (P: Term eT ⇒ Term bool) ≔
 //
 // Defined types
 //
-definition pred (eT: Univ Type) ≔ @prod Type Type eT (λ_, bool)
+definition pred (eT: Univ Type) ≔ prod eT (λ_, bool)
 definition PRED ≔ pred
 definition predicate ≔ pred
 definition PREDICATE ≔ pred
@@ -114,12 +115,6 @@ proof
 qed
 
 symbol reflexivity_of_equal T (x: Term T) : Term (eq x x)
-
-// FIXME: carrying builtins over import?
-set builtin "T" ≔ T
-set builtin "P" ≔ P
-// FIXME: could builtins be more flexible?
-// set builtin "eq" ≔ eq
 // set builtin "refl" ≔ reflexivity_of_equal
 
 symbol transitivity_of_equal T (x y z: Term T) :

prelude/cert_f/numbers.lp

@@ -47,7 +47,9 @@ definition nzreal ≔ nonzero_real
 
 symbol closed_plus_real: ∀(x y: Term real),
   let pr ≔ S.restr numfield real_pred in
-  Term (real_pred ((↑ numfield pr x) + (↑ numfield pr y)))
+  let xnf ≔ ↑ numfield pr x in
+  let ynf ≔ ↑ numfield pr y in
+  Term (real_pred (xnf + ynf))
 
 
 symbol lt (x y: Term real): Term bool