Skip to content

Commit 1b3c7ad

Browse files
committed
[docs] Add references to the Idris2 tutorial
Serves as a much more thorough introduction than the crash course, and we should definitely be pointing people more in that direction.
1 parent 2aebd29 commit 1b3c7ad

File tree

2 files changed

+12
-2
lines changed

2 files changed

+12
-2
lines changed

src/content/pages/docs/index.rst

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,11 @@ This includes:
1414
* `Changes required <https://idris2.readthedocs.io/en/latest/typedd/typedd.html>`_
1515
to the code in `Type Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_.
1616

17+
The
18+
`community-maintained Idris2 tutorial <https://idris-community.github.io/idris2-tutorial/>`_
19+
(originally written by Stefan Höck for undergraduate university teaching) is an
20+
excellent entry-point.
21+
1722
There is API documentation for the following packages:
1823

1924
* `prelude <https://www.idris-lang.org/Idris2/prelude>`__

src/content/pages/example.rst

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
Example
22
=======
33

4-
:date: 2020-04-01 11:00
4+
:date: 2025-10-16 17:30
55

66
Idris is a purely functional programming language, with first class types
77
- meaning that types are first class language constructs, and can be computed,
@@ -91,7 +91,12 @@ lengths of the inputs:
9191
app Nil ys = ys
9292
app (x :: xs) ys = x :: app xs ys
9393

94-
For more details, see `the tutorial <https://idris2.readthedocs.io/en/latest/tutorial/index.html>`_.
94+
For more details and quickly getting up to speed, there is
95+
`the "Crash Course in Idris2" <https://idris2.readthedocs.io/en/latest/tutorial/index.html>`_.
96+
97+
For a more beginner-friendly tutorial, please see
98+
`the community-maintained Idris2 tutorial <https://idris-community.github.io/idris2-tutorial/>`_,
99+
originally written by Stefan Höck for undergraduate university teaching.
95100

96101
Talks
97102
-----

0 commit comments

Comments
 (0)