实现说明
备注
Idris 的文档已在知识共享 CC0 许可下发布。因此，在法律允许的范围内，Idris 社区 已经放弃了 Idris 文档的所有版权和相关或邻近的权利。
关于CC0的更多信息，可以在网上找到：http://creativecommons.org/publicdomain/zero/1.0/
本节包含（或希望包含）关于 Idris 2 实现方面的各种注释，希望它们有助于调试和未来的贡献。
备注
Idris 的文档已在知识共享 CC0 许可下发布。因此，在法律允许的范围内，Idris 社区 已经放弃了 Idris 文档的所有版权和相关或邻近的权利。
关于CC0的更多信息，可以在网上找到：http://creativecommons.org/publicdomain/zero/1.0/
本节包含（或希望包含）关于 Idris 2 实现方面的各种注释，希望它们有助于调试和未来的贡献。