idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 17:21:59 +03:00
Code Issues Projects Releases Wiki Activity

Update typedd.rst

Browse Source
This commit is contained in:
J. Rinaldi 2024-06-15 11:42:04 +02:00 committed by G. Allais
parent 055568be28
commit 866354fef1
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
docs/source/typedd/typedd.rst
View File

@ -37,6 +37,8 @@ In ``Average.idr``, add:
import Data.List -- for `length` on lists import Data.List -- for `length` on lists
import System.REPL -- for `repl` import System.REPL -- for `repl`
Instead of entering ``6.0 + 3 * 12``, enter ``the Double (6.0 + 3 * 12)``.
In ``AveMain.idr`` and ``Reverse.idr`` add: In ``AveMain.idr`` and ``Reverse.idr`` add:
.. code-block:: idris .. code-block:: idris