内部语法注释中的双引号

Question

当将"字符放在Isabelle的内部语法的双引号部分的注释中时，其行为不像我所期望的那样。澄清一下:在下面的函数定义中，我希望the "at" sign被解析为注释。事实上，Isabelle将注释中的第一个"字符与该行开头的"字符匹配，从而导致语法错误。

fun reverse where 
  "reverse [] = []"
| "reverse (x#xs) = reverse xs @ (* the "at" sign *) [x]"

我可以通过写(* the 'at' sign *)来解决这个限制，但我更想了解到底发生了什么。那么在Isabelle术语中写这种评论的正确方法是什么呢?

Answer 1

我想它会与转义字符一起工作，如" ?