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

use*_*393 5 string character notation coq

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

Art*_*rim 2

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

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

Check 'a'.
Check 'c'.
Run Code Online (Sandbox Code Playgroud)

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