Refactor type level example and change it to use infix operators

Author: polytypic

examples/type-level.1ml

@@ -28,8 +28,8 @@ TypeLevel: {
 
     not: t -> t
 
-    andAlso: t -> t -> t
-    orElse: t -> t -> t
+    (&&&): t -> t -> t
+    (|||): t -> t -> t
 
     equals: t -> t -> t
   }
@@ -43,7 +43,7 @@ TypeLevel: {
     isL: t -> Bool.t
     isR: t -> Bool.t
 
-    case: t -> t
+    case: (type _ _) -> (type _ _) -> t -> type
   }
 
   Nat: {
@@ -55,6 +55,7 @@ TypeLevel: {
     one: t
 
     succ: t -> t
+
     (+): t -> t -> t
     (*): t -> t -> t
   }
@@ -80,10 +81,9 @@ TypeLevel: {
 
     type of fst snd: t = fun (type d _ _) => d fst snd
 
-    type cross (type f _) (type s _) (p: t): t = fun (type d _ _) =>
-      of (f (fst p)) (s (snd p)) d
+    type cross (type f _) (type s _) (p: t): t = of (f (fst p)) (s (snd p))
 
-    type map (type f _) (p: t): t = fun (type d _ _) => cross f f p d
+    type map (type f _) (p: t): t = cross f f p
   }
 
   Bool = {
@@ -94,8 +94,8 @@ TypeLevel: {
 
     type not (x: t): t = fun true false => x false true
 
-    type andAlso (l: t) (r: t): t = fun false true => l (r true false) false
-    type  orElse (l: t) (r: t): t = fun false true => l true (r true false)
+    type (l: t) &&& (r: t): t = fun false true => l (r true false) false
+    type (l: t) ||| (r: t): t = fun false true => l true (r true false)
 
     type equals (l: t) (r: t): t =
       fun true false => l (r true false) (r false true)
@@ -112,7 +112,7 @@ TypeLevel: {
     type isR (a: t): Bool.t =
       fun true false => a (fun _ => false) (fun _ => true)
 
-    type case (a: t) (type inL _) (type inR _) = a inL inR
+    type case (type inL _) (type inR _) (a: t): type = a inL inR
   }
 
   Nat = {
@@ -121,11 +121,12 @@ TypeLevel: {
     type isZero (n: t): Bool.t = fun true false => n (fun _ => false) true
 
     type zero: t = fun (type _    _) zero => zero
-    type  one: t = fun (type succ _) zero => succ zero
+    type  one: t = fun (type succ _) => succ
 
-    type     succ (n: t): t = fun (type succ _) zero => succ (n succ zero)
     type (m: t) + (n: t): t = fun (type succ _) zero => n succ (m succ zero)
-    type (m: t) * (n: t): t = fun (type succ _) zero => n (m succ) zero
+    type (m: t) * (n: t): t = fun (type succ _) => n (m succ)
+
+    type succ = (+) one
   }
 
   List = {