cleaning up examples

example/comparable.msph

@@ -0,0 +1,16 @@
+nominal lt
+nominal eq
+nominal gt
+
+type ord = lt | eq | gt
+
+type comparable[t] = {
+	member cmp : t -> ord
+}
+
+
+type integer = {
+	member cmp : integer -> ord
+}
+
+assert integer <: comparable[integer]

example/ex1.msph

@@ -1,4 +0,0 @@
-
-nominal C
-
-

example/ex2.msph

@@ -1 +0,0 @@
-type A = & C D

example/ex3.msph

@@ -1,13 +0,0 @@
-
-type X = & C (| D E)
-
-type Y = {
-	member x : X
-	type Z = & X {
- 		type T = C
-		assert C <: D
-	}
-	member r : (box forall S. (=> S Y))
-	member s : C[X, Y, z]
-	member f : -> A B
-}

example/ex4.msph

@@ -1,20 +0,0 @@
-nominal M
-nominal N
-nominal O
-nominal P
-
-type A = {
-	member member1: & N M
-	member member2: | M N
-}
-
-type B = forall X. {
-	member member1 : & X A
-}
-
-member outer1 : box {
-	member member1: & B True
-	type T = & B A
-	member member2 : | (& T O) P
-	type S = & B False
-}

example/ex5.msph

@@ -1,21 +0,0 @@
-nominal N
-nominal M
-
-
-type T[X, Y] = {
-	// body
-}
-
-type A = T[N, M] // binding X -> N, Y -> M
-type B = T[M, N] // binding X -> M, Y -> N
-
-// converted to
-
-type A = ⟨ X -> N, Y -> M ⟩ {
-	// body
-}
-type B = ⟨ X -> M, Y -> N ⟩ {
-	// body
-}
-
-

example/graph.msph

@@ -0,0 +1,10 @@
+type gnode[e] = {
+	member edges : iterable[e]
+}
+
+type gedge[n] = {
+	member src : n
+	member dst : n
+}
+
+type graph[n, e] = (n <: gnode[e]) & (e <: gedge[n])

example/non-parse/ex6.msph

@@ -1,21 +0,0 @@
-type A[X, Y] = {
-	type B[Z] = {
-		mb : X & Z
-	}
-
-	ma : B[Y]
-}
-
-
-m : A[M, N]
-
-
-m : ⟨X -> M, Y -> N⟩ {
-	ma : B[Y]
-}
-
-m : ⟨X -> M, Y -> N⟩ {
-	ma : ⟨Z -> Y⟩  {
-		mb : X & Z
-	}
-}

example/self.msph

@@ -0,0 +1,19 @@
+type Accumulator[Self] = (Self <: Accumulator[Self]) & {
+	member add : Int -> Self
+}
+
+type MyAccum = {
+	member add : Int -> MyAccum
+}
+
+assert MyAccum <: Accumulator[MyAccum]
+
+
+
+
+
+type Acchmmmmulator[Self] = (Self <: Acchmmmmulator[Self]) => {
+	member add : Int -> Self
+}
+
+