伊德里斯的实例
是否有任何Idris的例子可以用来研究，或者将它用于通用/“现实世界”的应用？
我在Haskell方面非常精通，Idris似乎借用了很多，官方FAQ /文档相当不错，但是有一些更大的例子可以帮助我们探索。 目标是尝试使用Idris进行实际的软件开发。 TIA。
Edwin Brady在https://github.com/edwinb/idris-demos上有一个充满演示的回购。; 除此之外，它还有一个可玩的空间入侵者游戏，使用SDL绑定，效果和！-effect语法编写（基本上是do_otation / >> =的替代语法）。
另外，我们试图维护wiki上一些可用库的列表： https ： //github.com/idris-lang/Idris-dev/wiki/Libraries
Idris的创build者Edwin Brady撰写了一篇关于效率和并发性等现实世界问题的论文： “通过构build正确的并发性：使用依赖types来validation有效资源使用协议的实现” 。 它不仅解释了如何处理并发，还在Idris中创build了一个embedded式域特定语言（EDSL）来处理并发。
它也被用于科学计算（可能或不可能被认为是现实世界的应用）： 科学计算中的依赖型编程 。 本文包含实际的例子和几个Agda的例子。
