0

Ltac 用于自动证明和修改证明环境、输出字符串和定义复杂的符号。它也可以用于 Coq 环境的“智能”修改吗？以下是两次失败的尝试：

Variable Phy: Set.

Fail Let pp (x:Type) := ltac: (match type of x with
       | Set => constr: (Reset Phy)
       | _ => idtac end).
(*Cannot infer an internal placeholder of type "Type" in environment: x : Type*)

Fail Ltac pp x := match type of x with
       | Set => constr: (Reset Phy)
       | _ => idtac end.
(*The reference Reset was not found in the current environment.*)

另外，如果这不是 Ltac 的工作，也许还有另一种方法？

4

1 回答 1

2

简短的回答：没有。

即使您可以使用一些 hack 来实现这一点，它也会在下一个 Coq 版本中停止工作。

原因是 ltac 命令的解释发生在比文档解释更低的级别。这个选择可能是有争议的，但它就是这样。策略在一个恒定的环境中运行，并且只能访问证明。因此，您可以从 ltac 做的最多的事情就是修改当前的证明。

发生您的错误是因为Reset确实在 ltac 无法访问的更高级别上进行了解析。

对于环境和文档本身的编程操作，您需要依赖 ML 代码，或者您可以尝试编写一些接口工具（例如 SerAPI）来实现您想要的。

于 2017-03-17T20:31:57.560 回答