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的解析器有任何負面影響。

Answer 2

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