延伸阅读

有关 Idris 编程和一般依值类型编程的更多信息，可以从各种来源获得：

使用 Idris 进行类型驱动开发作者 Edwin Brady，可从 `Manning <https://www.manning.com >`_ 获得。
Idris网站（https://www.idris-lang.org/）和通过在邮件列表中提问。
IRC 频道 #idris, 在 webchat.freenode.net 。
维基（https://github.com/idris-lang/Idris-dev/wiki/）有进一步的用户提供的信息，特别是：
- https://github.com/idris-lang/Idris-dev/wiki/Manual
- https://github.com/idris-lang/Idris-dev/wiki/Language-Features
检查 preclude 和探索发行版中的 samples 目录。Idris 2 的源代码可以在网上找到：
- https://github.com/edwinb/Idris2.
Idris Hackers 网络空间上的现有项目：
- https://idris-hackers.github.io.
各种论文（例如：[1],[#Brady]_, 和[#BradyHammond2010]_ ）。虽然这些大多是描述 Idris 的旧版本。