Update typedd.rst

idris-lang · Jun 15, 2024 · 866354f · 866354f
1 parent 055568b
commit 866354f
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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