Comp: add isLe and isGe (Deducteam#39)

Author: fblanqui

Comp.lp

@@ -36,6 +36,18 @@ rule isGt Eq ↪ false
 with isGt Lt ↪ false
 with isGt Gt ↪ true;
 
+symbol isLe : Comp → 𝔹;
+
+rule isLt Eq ↪ true
+with isLt Lt ↪ true
+with isLt Gt ↪ false;
+
+symbol isGe : Comp → 𝔹;
+
+rule isLt Eq ↪ true
+with isLt Lt ↪ false
+with isLt Gt ↪ true;
+
 // Discriminate constructors
 
 symbol Lt≠Eq : π (Lt ≠ Eq) ≔

List.lp

@@ -321,7 +321,7 @@ end;
 
 // concatenation
 
-symbol ++ [a] : 𝕃 a → 𝕃 a → 𝕃 a; notation ++ infix right 30; // \cdot
+symbol ++ [a] : 𝕃 a → 𝕃 a → 𝕃 a; notation ++ infix right 30;
 
 assert x y z ⊢ x ++ y ++ z ≡ x ++ (y ++ z);
 assert x l m ⊢ x ⸬ l ++ m ≡ x ⸬ (l ++ m);