git.iko.soy/Idris-dev
on master help sign in
Change name of Err to Error (#3187)

Running through this example I got a name clash with the Err type. ``` - + Errors (1) `-- Btree.idr line 61 col 12: When checking type of Main.parseNumber: Can't disambiguate name: Language.Reflection.Errors.Err, Main.Err ``` Changing the name to Error doesn't seem to have the same issue. I have the following packages loaded in the emacs-idris-repl ```elisp -- Local Variables: -- idris-load-packages: ("prelude" "base" "effects") -- End: ```

commit4dc2a6a4328302a6807c184ef56b1c6002e0c86c authorTim McGilchrist <timmcgil@gmail.com> dateWed 25 May 2016, 12:00 (10 years ago) parentbc5d9d4
1 file changed+10−10
compare with master
unifiedsplit
docs/effects/simpleeff.rst+10−10
docs/effects/simpleeff.rst+10−10
@@ -165,9 +165,9 @@ parameterised by an error type:
165165
166166.. code-block:: idris
167167
168− data Err = NotANumber | OutOfRange
168+ data Error = NotANumber | OutOfRange
169169
170− parseNumber : Int -> String -> Eff Int [EXCEPTION Err]
170+ parseNumber : Int -> String -> Eff Int [EXCEPTION Error]
171171 parseNumber num str
172172 = if all isDigit (unpack str)
173173 then let x = cast str in
@@ -178,23 +178,23 @@ parameterised by an error type:
178178
179179Programs which support the ``EXCEPTION`` effect can be run in any
180180context 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
182182the form ``Right x`` if successful:
183183
184184.. code-block:: idris
185185
186− *Exception> the (Either Err Int) $ run (parseNumber 42 "20")
187− Right 20 : Either Err Int
186+ *Exception> the (Either Error Int) $ run (parseNumber 42 "20")
187+ Right 20 : Either Error Int
188188
189189Or ``Left e`` on failure, carrying the appropriate exception:
190190
191191.. code-block:: idris
192192
193− *Exception> the (Either Err Int) $ run (parseNumber 42 "50")
194− Left OutOfRange : Either Err Int
193+ *Exception> the (Either Error Int) $ run (parseNumber 42 "50")
194+ Left OutOfRange : Either Error Int
195195
196− *Exception> the (Either Err Int) $ run (parseNumber 42 "twenty")
197− Left NotANumber : Either Err Int
196+ *Exception> the (Either Error Int) $ run (parseNumber 42 "twenty")
197+ Left NotANumber : Either Error Int
198198
199199In fact, we can do a little bit better with ``parseNumber``, and have
200200it return a *proof* that the integer is in the required range along
@@ -222,7 +222,7 @@ the boundedness proof:
222222
223223.. code-block:: idris
224224
225− parseNumber : (x : Int) -> String -> Eff (Bounded x) [EXCEPTION Err]
225+ parseNumber : (x : Int) -> String -> Eff (Bounded x) [EXCEPTION Error]
226226 parseNumber x str
227227 = if all isDigit (unpack str)
228228 then let num = cast str in