Coq 中字符的单引号表示法？

Question

在大多数编程语言中，'c'是一个字符，"c"也是一个长度为 1 的字符串。但是 Coq（根据其标准 ascii 和字符串库）使用"c"这两者作为表示法，这需要不断使用 来Open Scope明确所指的是哪一个。如何避免这种情况并以通常的方式用单引号指定字符？如果有一个解决方案仅部分覆盖标准库，更改表示法但回收其余部分，那就太好了。

Answer 1

我非常有信心没有聪明的方法可以做到这一点，但有一个有点烦人的方法：简单地为每个字符声明一个符号。

Notation "''c''" := "c" : char_scope.
Notation "''a''" := "a" : char_scope.

Check 'a'.
Check 'c'.

编写自动生成这些声明的脚本应该不会太难。不过，我不知道这是否会对 Coq 的解析器产生任何负面影响。