在大多数编程语言中，'c'是一个字符和 "c"是长度为 1 的字符串。但是 Coq(根据其标准 ascii 和字符串库)使用 "c"作为两者的符号，这需要不断使用 Open Scope澄清指的是哪一个。您如何避免这种情况并以通常的方式使用单引号指定字符？如果有一个仅部分覆盖标准库的解决方案，更改符号但回收其余部分，那就太好了。
最佳答案
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").
关于string - Coq 中字符的单引号表示法？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/26112349/