CODEWITHSUNDEEP
stringcharactercoqnotation
user287393
user287393

Reputation: 1241

Single-quote notation for characters in Coq?

In most programming languages, 'c' is a character and "c" is a string of length 1. But Coq (according to its standard ascii and string library) uses "c" as the notation for both, which requires constant use of Open Scope to clarify which one is being referred to. How can you avoid this and designate characters in the usual way, with single quotes? It would be nice if there is a solution that only partially overrides the standard library, changing the notation but recycling the rest.

Upvotes: 5

Views: 838

Answers (2)

larsr
larsr

Reputation: 5811

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

or this

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

Check (c"A").
Check ("A").

Upvotes: 4

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

I am quite confident that there is no smart way of doing this, but there is a somewhat annoying one: simply declare one notation for each character.

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

Check 'a'.
Check 'c'.

It shouldn't be too hard to write a script for automatically generating those declarations. I don't know if this has any negative side-effects on Coq's parser, though.

Upvotes: 2

Related Questions