diff --git a/docs/source/typedd/typedd.rst b/docs/source/typedd/typedd.rst index 0e0666d739..2a198c61c7 100644 --- a/docs/source/typedd/typedd.rst +++ b/docs/source/typedd/typedd.rst @@ -37,6 +37,8 @@ In ``Average.idr``, add: import Data.List -- for `length` on lists 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: .. code-block:: idris