From ca071a96c3f154890fdfa5aea8c914b289993496 Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Wed, 10 Mar 2021 18:27:05 +0600 Subject: [PATCH] [ docs ] Update Control.App docs --- docs/source/app/interfaces.rst | 2 +- docs/source/app/introapp.rst | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/source/app/interfaces.rst b/docs/source/app/interfaces.rst index 11d6b9a9e..553937a2e 100644 --- a/docs/source/app/interfaces.rst +++ b/docs/source/app/interfaces.rst @@ -50,7 +50,7 @@ use ``PrimIO`` in the initial list of errors ``Init``. .. code-block:: idris - HasErr Void e => PrimIO e where ... + HasErr AppHasIO e => PrimIO e where ... Given this, we can implement ``Console`` and run our ``hello`` program in ``IO``. It is implemented as follows in ``Control.App.Console``: diff --git a/docs/source/app/introapp.rst b/docs/source/app/introapp.rst index de756efa3..9997eca18 100644 --- a/docs/source/app/introapp.rst +++ b/docs/source/app/introapp.rst @@ -95,7 +95,7 @@ synonym for ``Type``): .. code-block:: idris Init : List Error - Init = [Void] + Init = [AppHasIO] run : App {l} Init a -> IO a @@ -103,5 +103,5 @@ Generalising the ``Path`` parameter with ``l`` means that we can invoke ``run`` for any application, whether the ``Path`` is ``NoThrow`` or ``MayThrow``. But, in practice, all applications given to ``run`` will not throw at the top level, because the only -exception type available is the empty type ``Void``. Any exceptions +exception type available is the type ``AppHasIO``. Any exceptions will have been introduced and handled inside the ``App``.