根据文档，可以定义打印符号的格式:https://coq.inria.fr/refman/Reference-Manual014.html sec530
但是，可以定义如下的符号:
Notation " '[[' a ']]' b " := (* something *).
目前还不清楚两者是否可以相互作用。尝试:
format " '[hv' '[[' a ']]' ']' b "
会触发Coq，因为它期望方括号后面跟着、hv和metasyntax:parse_format之一。
到目前为止，我所尝试的任何其他类型的转义都使Coq以不匹配符号的形式拒绝该格式。
你的朋友是[[ https://github.com/coq/coq/blob/trunk/toplevel/metasyntax.ml#L102
正如您在代码中看到的那样，您的具体方案将无法工作。我不知道是否有一些特殊的技巧，现在你必须停止使用双括号。
我敢肯定，Coq上游会考虑在CC_6中添加parse_quoted案例的补丁。
希望8.7能在这方面带来一些改进，CEP#9尝试提出替换/进化反解析到一个真正的基于盒的模型。