Clever Geek Handbook

Single quote for characters in Coq?

In most programming languages, it 'c'

is a symbol, and "c"

is a string of length 1. But Coq (according to its standard ascii and string library) uses "c"

as a notation for both, which requires constant use Open Scope

to clarify who it refers to. How can you avoid this and denote characters in the usual way with single quotes? It would be nice if there was a solution that only partially overrides the standard library by changing the notation but reworking the rest.

+3


source to share


2 answers


I'm pretty sure there isn't a sane way to do this, but there is a somewhat annoying one: just declare one notation for each character.

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

Check 'a'.
Check 'c'.


No script can be written to generate these declarations automatically. I don't know if this has any negative side effects for the Coq parser.

+1


source 


Require Import Ascii.
Require Import String.
Check "a"%char.
Check "b"%string.

or



Program Definition c (s:string) : ascii :=
match s with "" => " "%char | String a _ => a end.

Check (c"A").
Check ("A").
+1


source






More articles:


All Articles