regex - Idris 中是否支持正则表达式？

Question

我在 Idris 文档中没有看到正则表达式，它是否以任何（最好是可移植的）方式支持？还是计划好的？

Answer 1

Idris 文档没有提到内置的正则表达式引擎。（有趣的是，Haskell 有一个正则表达式模块。）Idris 手册页指出它可能缺少很多东西：

值得注意的是，Idris 首先是一个研究工具和项目。因此，提供的工具和创建的结果程序不一定被视为生产就绪或工业用途。

因此，使用IdrisScript似乎是一种相关的解决方法。

Answer 2

这是我在 Idris 中的正则表达式匹配工具。

使用导数的概念证明匹配算法是正确的。希望它能有所帮助。