@@ -61,8 +61,8 @@ answer. For example:
6161 True : Bool
6262
6363All of the usual arithmetic and comparison operators are defined for
64−the primitive types. They are overloaded using type classes, as we
65−will discuss in Section :ref:`sect-classes` and can be extended to
64+the primitive types. They are overloaded using interfaces, as we
65+will discuss in Section :ref:`sect-interfaces` and can be extended to
6666work on user defined types. Boolean expressions can be tested with the
6767``if...then...else`` construct, for example:
6868
@@ -162,7 +162,7 @@ Idris prompt:
162162 4 : Nat
163163
164164Like arithmetic operations, integer literals are also overloaded using
165−type classes, meaning that we can also test the functions as follows:
165+interfaces, meaning that we can also test the functions as follows:
166166
167167::
168168
@@ -475,15 +475,16 @@ Sometimes it is useful to provide types of implicit arguments,
475475particularly where there is a dependency ordering, or where the
476476implicit arguments themselves have dependencies. For example, we may
477477wish to state the types of the implicit arguments in the following
478−definition, which defines a predicate on vectors:
478+definition, which defines a predicate on vectors (this is also defined
479+in ``Data.Vect``, under the name ``Elem``):
479480
480481.. code-block:: idris
481482
482− data Elem : a -> Vect n a -> Type where
483− Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
484− There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
483+ data IsElem : a -> Vect n a -> Type where
484+ Here : {x:a} -> {xs:Vect n a} -> IsElem x (x :: xs)
485+ There : {x,y:a} -> {xs:Vect n a} -> IsElem x xs -> IsElem x (y :: xs)
485486
486−An instance of ``Elem x xs`` states that ``x`` is an element of
487+An instance of ``IsElem x xs`` states that ``x`` is an element of
487488``xs``. We can construct such a predicate if the required element is
488489``Here``, at the head of the vector, or ``There``, in the tail of the
489490vector. For example:
@@ -493,7 +494,7 @@ vector. For example:
493494 testVec : Vect 4 Int
494495 testVec = 3 :: 4 :: 5 :: 6 :: Nil
495496
496− inVect : Elem 5 testVec
497+ inVect : IsElem 5 testVec
497498 inVect = There (There Here)
498499
499500If the same implicit arguments are being used a lot, it can make a
@@ -504,9 +505,9 @@ appear within the block:
504505.. code-block:: idris
505506
506507 using (x:a, y:a, xs:Vect n a)
507− data Elem : a -> Vect n a -> Type where
508− Here : Elem x (x :: xs)
509− There : Elem x xs -> Elem x (y :: xs)
508+ data IsElem : a -> Vect n a -> Type where
509+ Here : IsElem x (x :: xs)
510+ There : IsElem x xs -> IsElem x (y :: xs)
510511
511512Note: Declaration Order and ``mutual`` blocks
512513~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -579,14 +580,14 @@ example for reading and writing files, including:
579580 data File -- abstract
580581 data Mode = Read | Write | ReadWrite
581582
582− openFile : String -> Mode -> IO File
583+ openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
583584 closeFile : File -> IO ()
585+
586+ fGetLine : (h : File) -> IO (Either FileError String)
587+ fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
588+ fEOF : File -> IO Bool
584589
585− fread : File -> IO String
586− fwrite : File -> String -> IO ()
587− feof : File -> IO Bool
588−
589− readFile : String -> IO String
590+Note that several of these return ``Either``, since they may fail.
590591
591592.. _sect-do:
592593
@@ -724,8 +725,7 @@ the vector:
724725 *usefultypes> show (map double intVec)
725726 "[2, 4, 6, 8, 10]" : String
726727
727−You’ll find these examples in ``usefultypes.idr`` in the ``examples/``
728−directory. For more details of the functions available on ``List`` and
728+For more details of the functions available on ``List`` and
729729``Vect``, look in the library files:
730730
731731- ``libs/prelude/Prelude/List.idr``