Are*_*lis 6 theorem-proving idris
如果我理解正确(主要来自applyTactic函数的存在),就可以为Idris中的定理证明者编写自定义策略.我可以用什么(或在哪里)学习如何做到这一点？
在伊德里斯有两种编写自定义策略的机制:高级和低级反思.
使用高级反射,您可以编写一个在语法而不是在评估数据上运行的函数 - 它不会减少其参数.这些功能返回了一种新的策略,使用伊德里斯现有的战术定义.如果您想直接返回证明条款,您可以随时使用Exact.可以在效果库中找到这种反射的示例.byReflection在证明模式下使用高级反射策略.
在低级反思中,您可以直接使用Idris核心类型理论中的引用术语.然后,策略是TT -> List (TTName, TT) -> Tactic第一个参数是目标类型的函数,第二个是本地证明上下文,返回结果与高级反射相同.这就是上面所说的laughadelic .这些applyTactic在证明模式下使用.