伊德里斯的自定义证明战术

Question

如果我理解正确（主要是从存在的 applyTactic 函数），可以为idris中的定理证明者编写自定义策略。什么（或在哪里）是我可以用来学习如何做到这一点的一些例子？

Answer 1

在Idris中编写自定义策略有两种机制:高层次和低层次的反射。

使用高级反射，您编写一个在语法上运行而不是在评估数据上运行的函数-它不会减少其参数。这些函数返回一个新的战术，使用Idris中预先存在的战术定义。如果你想直接返回一个证明术语，你总是可以使用 Exact.这种反射的一个例子可以在 效果库.使用以下方法调用高级反射策略 byReflection 在证明模式。

在低级反射中，您直接使用Idris核心类型理论中的引用术语。一个策略就是一个功能 TT -> List (TTName, TT) -> Tactic 其中第一个参数是目标类型，第二个是局部证明上下文，返回结果与高级反射中的相同。这就是laughadelic与之相关的内容 以上.这些调用使用 applyTactic 在证明模式。