diff --git a/docs/source/typedd/typedd.rst b/docs/source/typedd/typedd.rst
index 2a198c61c7..287cc1a50d 100644
--- a/docs/source/typedd/typedd.rst
+++ b/docs/source/typedd/typedd.rst
@@ -60,6 +60,12 @@ match on:
     createEmpties : {n : _} -> Vect n (Vect 0 elem)
     transposeMat : {n : _} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
 
+For the same reason, we also need to change the type of ``length`` to:
+
+.. code-block:: idris
+
+    length : {n : _} -> Vect n elem -> Nat
+
 Chapter 4
 ---------