From ecd6d47ea0ea5e2662cbb84fad0421cd250171a6 Mon Sep 17 00:00:00 2001
From: "J. Rinaldi" <2664441+m-rinaldi@users.noreply.github.com>
Date: Sun, 16 Jun 2024 17:15:02 +0200
Subject: [PATCH] Update typedd.rst

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

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
 ---------