idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-20 17:18:26 +03:00
Code Issues Projects Releases Wiki Activity

Update typedd.rst

Browse Source
This commit is contained in:
J. Rinaldi 2024-06-16 17:15:02 +02:00 committed by G. Allais
parent 866354fef1
commit ecd6d47ea0
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
docs/source/typedd/typedd.rst
View File

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