Skip to content

Commit 72c6b00

Browse files
committed
[docs] Explicitly link the Idris2 tutorial
This is likely the closest one can come to a "Type-Driven Development with Idris **2**" book, so it should be near the top. Huge props to Stefan Höck for writing the original, and to the community for turning it into an mdBook and now having stewardship of it.
1 parent f496256 commit 72c6b00

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

docs/source/tutorial/conclusions.rst

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,9 @@ dependent types in general, can be obtained from various sources:
1010
* `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_
1111
by Edwin Brady, available from `Manning <https://www.manning.com>`_.
1212

13+
* `The community Idris2 tutorial <https://idris-community.github.io/idris2-tutorial/>`_,
14+
originally written by Stefan Höck, now maintained by the community.
15+
1316
* The Idris website (https://www.idris-lang.org/) has pointers to a broad range
1417
of resources.
1518

0 commit comments

Comments
 (0)