cosmetics

prelude/functions.lp

 require open personoj.encodings.cert_f
-personoj.adlib.bootstrap
-personoj.prelude.logic
+  personoj.adlib.bootstrap
+  personoj.prelude.logic
 require personoj.adlib.subtype as S
 
 //
@@ -11,14 +11,14 @@ require personoj.adlib.subtype as S
 // extensionality_postulate (D R: Term uType) (f g: Term (D ~> R))
 // : Term (biff (forall (λx: Term D, f x = g ) (f = g)))
 
-definition {|injective?|} {D} {R} (f: Term (D ~> R))
-  ≔ forall (λx1, forall (λx2, imp (f x1 = f x2) (x1 = x2)))
+definition {|injective?|} {D} {R} (f: Term (D ~> R)) ≔
+  forall (λx1, forall (λx2, imp (f x1 = f x2) (x1 = x2)))
 
-definition {|surjective?|} {D: Term uType} {R: Term uType} (f: Term (D ~> R))
-  ≔ forall (λy, ∃ (λx, (f x) = y))
+definition {|surjective?|} {D: Term uType} {R: Term uType} (f: Term (D ~> R)) ≔
+  forall (λy, ∃ (λx, (f x) = y))
 
-definition {|bijective?|} {D: Term uType} {R: Term uType} (f: Term (D ~> R))
-  ≔ ({|injective?|} f) ∧ ({|surjective?|} f)
+definition {|bijective?|} {D: Term uType} {R: Term uType} (f: Term (D ~> R)) ≔
+  ({|injective?|} f) ∧ ({|surjective?|} f)
 
 theorem bij_is_inj {D: Term uType} {R: Term uType}:
   Term (Psub {D ~> R} {|bijective?|} ⊑ Psub {D ~> R} {|injective?|})
@@ -37,13 +37,12 @@ rule domain {&D} {_} _ → &D
 // restrict[T: TYPE, S: TYPE FROM T, R: TYPE]
 //
 symbol restrict {T: Term uType} (S: Term uType) {R: Term uType}
-  (f: Term (T ~> R)) (_: Term (S ⊑ T)) (s: Term S)
-  : Term R
+                (f: Term (T ~> R)) (_: Term (S ⊑ T)) (s: Term S):
+  Term R
 rule restrict {&T} _ {_} &f &pr &s → &f (↑ &T &pr &s)
 
-theorem injective_restrict {T} S {R} (f: Term (T ~> R))
-  (pr: Term (S ⊑ T))
-  : Term ({|injective?|} f) ⇒ Term ({|injective?|} (restrict S f pr))
+theorem injective_restrict {T} S {R} (f: Term (T ~> R)) (pr: Term (S ⊑ T)):
+  Term ({|injective?|} f) ⇒ Term ({|injective?|} (restrict S f pr))
 proof
 admit
 
@@ -51,8 +50,8 @@ admit
 // restrict_props[T: TYPE, R: TYPE]
 //
 
-theorem restrict_full {T: Term uType} {R: Term uType} (f: Term (T ~> R))
-  : Term (eq {T ~> R} (restrict {T} T {R} f (S.refl T)) f)
+theorem restrict_full {T: Term uType} {R: Term uType} (f: Term (T ~> R)):
+  Term (eq {T ~> R} (restrict {T} T {R} f (S.refl T)) f)
 proof
 admit
 
@@ -61,9 +60,6 @@ admit
 //
 
 definition extend {T: Term uType}
-  (s_pred: Term (pred T))
-  {R: Term uType} (d: Term R)
-  (f: Term (Psub s_pred ~> R))
-  (t: Term T)
-  (pr: Term (s_pred t))
-  ≔ if (s_pred t) (f (↓ s_pred t pr)) d
+  (s_pred: Term (pred T)) {R: Term uType} (d: Term R)
+  (f: Term (Psub s_pred ~> R)) (t: Term T) (pr: Term (s_pred t)) ≔
+  if (s_pred t) (f (↓ s_pred t pr)) d

prelude/logic.lp

@@ -106,11 +106,10 @@ qed
 symbol reflexivity_of_equal T (x: Term T) : Term (eq x x)
 // set builtin "refl" ≔ reflexivity_of_equal
 
-symbol transitivity_of_equal T (x y z: Term T) :
+symbol transitivity_of_equal T (x y z: Term T):
   Term ((x = y) ∧ (y = z)) ⇒ Term (eq x z)
 
-symbol symmetry_of_equal T (x y: Term T):
-  Term (x = y) ⇒ Term (y = x)
+symbol symmetry_of_equal T (x y: Term T): Term (x = y) ⇒ Term (y = x)
 
 //
 // if_props