Update typedd.rst

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