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

Question

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

Answer 1

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").