Fix small typos

doc/examples/specification.md

@@ -123,7 +123,7 @@ of `intf.send` and it can update the monitor state.  In addition, the
 monitor inserts an assertion before every call to `intf.recv`. This
 assertion is introduced with the `require` statement. This means that
 the calling environment of `inft.recv` must guarantee that the
-condition `sent(x)` holds before the call to `intf.send`. That is, the
+condition `sent(x)` holds before the call to `intf.recv`. That is, the
 received packet `x` must previously have been sent.
 
 In effect, our service specification describes a channel that can

doc/examples/values.md

@@ -91,7 +91,7 @@ Here is an example of a simple program that tabulates the function
     instance arr : array(t,t)
 
     action tabulate(max : t) returns (res:arr.t) {
-        local i:index {
+        local i:t {
             i := 0;
             res := arr.create(max,0);
             while i < max {

doc/language.md

@@ -61,7 +61,7 @@ Every Ivy file begins with a line like the following:
 This tells Ivy what version of the language we are using. This is
 important because in successive version of the language, certain
 features may be changed or deprecated. Providing the language version
-allows old programs to keep working. They current version of the Ivy
+allows old programs to keep working. The current version of the Ivy
 language is 1.7. Changes between versions of the language are listed
 at the end of this document.
 

ivy/include/1.8/collections.ivy

@@ -98,11 +98,11 @@ module array(domain,range) = {
 	after create {
 	    assert end(a) = s & value(a,X) = y
 	}
-        before set {
+    before set {
 	    assert 0 <= x & x < end(a)
 	}	       	 
 	after set {
-            assert end(a) = end(old a);
+        assert end(a) = end(old a);
 	    assert value(a,X) = y if X = x else value(old a,X)
 	}
 	before get {