用于双方括号的 Coq 表示法格式

Question

根据文档，可以定义打印符号的格式： https://coq.inria.fr/refman/Reference-Manual014.html#sec530

但是，可以定义如下符号：

Notation " '[[' a ']]' b " := (* something *).

两者能否互动，目前还很不清楚。尝试：

format " '[hv' '[[' a ']]' ']' b "

例如，Coq 跳闸，因为它期望方括号后面跟着 、v 和 hv 之一。

到目前为止，我尝试过的任何其他类型的转义都会使 Coq 拒绝该格式，因为它与符号不匹配。

我不确定这是否可以做到......

Answer 1

你的朋友是metasyntax:parse_formathttps://github.com/coq/coq/blob/trunk/toplevel/metasyntax.ml#L102

正如您在代码中看到的那样，您的具体方案不起作用。我不知道是否有一些特定的技巧，现在你必须停止使用双括号。

不过，我确信 Coq 上游会考虑在 parse_quoted 中添加 [[ 案例的补丁。

希望 8.7 会带来一些改进，CEP#9 尝试提议将反解析替换/演变为真正的基于框的模型。