@@ -165,9 +165,9 @@ parameterised by an error type:
166.. code-block:: idris
166.. code-block:: idris
168− data Err = NotANumber | OutOfRange
168+ data Error = NotANumber | OutOfRange
170− parseNumber : Int -> String -> Eff Int [EXCEPTION Err]
170+ parseNumber : Int -> String -> Eff Int [EXCEPTION Error]
171 parseNumber num str
171 parseNumber num str
172 = if all isDigit (unpack str)
172 = if all isDigit (unpack str)
173 then let x = cast str in
173 then let x = cast str in
@@ -178,23 +178,23 @@ parameterised by an error type:
179Programs which support the ``EXCEPTION`` effect can be run in any
179Programs which support the ``EXCEPTION`` effect can be run in any
180context which has some way of throwing errors, for example, we can run
180context which has some way of throwing errors, for example, we can run
181−``parseNumber`` in the ``Either Err`` context. It returns a value of
181+``parseNumber`` in the ``Either Error`` context. It returns a value of
182the form ``Right x`` if successful:
182the form ``Right x`` if successful:
184.. code-block:: idris
184.. code-block:: idris
186− *Exception> the (Either Err Int) $ run (parseNumber 42 "20")
186+ *Exception> the (Either Error Int) $ run (parseNumber 42 "20")
187− Right 20 : Either Err Int
187+ Right 20 : Either Error Int
189Or ``Left e`` on failure, carrying the appropriate exception:
189Or ``Left e`` on failure, carrying the appropriate exception:
191.. code-block:: idris
191.. code-block:: idris
193− *Exception> the (Either Err Int) $ run (parseNumber 42 "50")
193+ *Exception> the (Either Error Int) $ run (parseNumber 42 "50")
194− Left OutOfRange : Either Err Int
194+ Left OutOfRange : Either Error Int
196− *Exception> the (Either Err Int) $ run (parseNumber 42 "twenty")
196+ *Exception> the (Either Error Int) $ run (parseNumber 42 "twenty")
197− Left NotANumber : Either Err Int
197+ Left NotANumber : Either Error Int
199In fact, we can do a little bit better with ``parseNumber``, and have
199In fact, we can do a little bit better with ``parseNumber``, and have
200it return a *proof* that the integer is in the required range along
200it return a *proof* that the integer is in the required range along
@@ -222,7 +222,7 @@ the boundedness proof:
223.. code-block:: idris
223.. code-block:: idris
225− parseNumber : (x : Int) -> String -> Eff (Bounded x) [EXCEPTION Err]
225+ parseNumber : (x : Int) -> String -> Eff (Bounded x) [EXCEPTION Error]
226 parseNumber x str
226 parseNumber x str
227 = if all isDigit (unpack str)
227 = if all isDigit (unpack str)
228 then let num = cast str in
228 then let num = cast str in