在大多数编程语言中，'c' 是一个字符，"c" 是一个长度为 1 的字符串。但是 Coq（根据其标准 ascii 和字符串库）使用 "c" 作为两者的符号，这需要常量使用Open Scope 来澄清所指的是哪一个。您如何避免这种情况并以通常的方式使用单引号指定字符？如果有一个解决方案只部分覆盖标准库，更改符号但回收其余部分，那就太好了。
【问题讨论】：
标签： string character coq notation
Require Import Ascii.
Require Import String.
Check "a"%char.
Check "b"%string.
或者这个
Program Definition c (s:string) : ascii :=
match s with "" => " "%char | String a _ => a end.
Check (c"A").
Check ("A").
【讨论】：
我非常确信没有聪明的方法可以做到这一点，但有一个有点烦人的方法：只需为每个字符声明一个符号。
Notation "''c''" := "c" : char_scope.
Notation "''a''" := "a" : char_scope.
Check 'a'.
Check 'c'.
编写一个自动生成这些声明的脚本应该不会太难。不过，我不知道这对 Coq 的解析器是否有任何负面影响。
【讨论】：