From 866354fef1ebfae5aae9003eb907f560d14cfc0f Mon Sep 17 00:00:00 2001
From: "J. Rinaldi" <2664441+m-rinaldi@users.noreply.github.com>
Date: Sat, 15 Jun 2024 11:42:04 +0200
Subject: [PATCH] Update typedd.rst

---
 docs/source/typedd/typedd.rst | 2 ++
 1 file changed, 2 insertions(+)

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