Fix 2 failing examples (#263) (#264)

Author: BinderDavid

examples/nonDeterminism.gr

@@ -6,10 +6,10 @@ import Vec
 return : forall {a : Type} . a -> Vec 1 a
 return x = Cons x Nil
 
-join : forall {a : Type, b : Type, n m : Nat}
+joinM : forall {a : Type, b : Type, n m : Nat}
     . Vec n (Vec m a) -> Vec (n * m) a
-join Nil = Nil;
-join (Cons xs xss) = xs `append` (join xss)
+joinM Nil = Nil;
+joinM (Cons xs xss) = xs `append` (joinM xss)
 
 -- Functor operation
 fmap : forall {a : Type, b : Type, n : Nat}
@@ -20,7 +20,7 @@ fmap [f] (Cons x xs) = Cons (f x) (fmap [f] xs)
 -- Derived bind operation
 bind : forall {a : Type, b : Type, n m : Nat}
      . Vec n a -> (a -> Vec m b) [n] -> Vec (n * m) b
-bind x f = join (fmap f x)
+bind x f = joinM (fmap f x)
 
 ---------------------------------------------------
 

examples/pad_left.gr

@@ -1,13 +1,5 @@
 import Vec
 
-monus
-  : forall {m n : Nat}
-  . N m -> N n -> N (m - n)
-monus m Z = m;
-monus Z (S n') = monus Z n';
-monus (S m') (S n') = monus m' n'
-
-
 pad_left
   : ∀ {a : Type, m : Nat, n : Nat}
   . a [n - m]