idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 04:33:45 +03:00
Code Issues Projects Releases Wiki Activity

Update introapp.rst

Browse Source 
Further explain why the App passed to ``run`` can't throw an exception.
This commit is contained in:
Tim Engler 2022-11-06 09:34:13 +08:00 committed by G. Allais
parent c6a8c9e7a7
commit 69f680e10a
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
docs/source/app/introapp.rst
View File

@ -103,5 +103,6 @@ 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 type ``AppHasIO``. Any exceptions
will have been introduced and handled inside the ``App``.
exception type available is the type ``AppHasIO``, which is an empty data
type (it has no values). Any exceptions will have been introduced and handled
inside the ``App``.