mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 04:33:45 +03:00
Fix documentation link in typesfuns tutorial
This commit is contained in:
parent
5beda25da6
commit
0a24821429
@ -716,8 +716,8 @@ Useful Data Types
|
||||
|
||||
Idris includes a number of useful data types and library functions
|
||||
(see the ``libs/`` directory in the distribution, and the
|
||||
`documentation <https://www.idris-lang.org/documentation/>`_). This section
|
||||
describes a few of these, and how to import them.
|
||||
`documentation <https://www.idris-lang.org/pages/documentation.html>`_). This
|
||||
section describes a few of these, and how to import them.
|
||||
|
||||
``List`` and ``Vect``
|
||||
---------------------
|
||||
|
Loading…
Reference in New Issue
Block a user