The Coq mailing list

[James Smith <jecs AT imperial.ac.uk>]

Hi,

I'm reading the documentation on Gallina here:

https://coq.inria.fr/distrib/current/refman/Reference-Manual003.html#note1

I'm not quite sure about the use of Unicode for defining identifiers. 
The specification is:

first_letter                ::=    a..z ∣ A..Z ∣ _ ∣ unicode-letter
subsequent_letter    ::=    a..z ∣ A..Z ∣ 0..9 ∣ _ ∣ ’ ∣ unicode-letter 
∣ unicode-id-part
ident                         ::=    first_letter 
[subsequent_letter…subsequent_letter]

Below it says:

" The entry unicode-letter non-exhaustively includes Latin, Greek, 
Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana and 
Katakana characters, CJK ideographs, mathematical letter-like symbols, 
hyphens, non-breaking space, … "

This doesn't seem to be very precise? It seems the exact range of what 
to match is left to the implementer. There are several Latin blocks, for 
example. Why the presence of non-breaking space? And why the ellipsis? 
I'm surprised to see that in a formal specification...

Similarly:

"The entry unicode-id-part non-exhaustively includes symbols for prime 
letters and subscripts."

I'm not sure what a prime letter is?

Probably it's just my ignorance but I would appreciate some help! What 
I'm thinking of doing in a meantime is just finding the most relevant 
Unicode blocks for the terms that I can at least recognise.

Kind regards,

James