I was trying to understand the way strings are represented (
string type) in coq.
Where is the notation that allows strings to made like
Check "hello%string. Check "a"%string.
Is it a normal notation or is it something special?
Was wondering about this as the
Notation command itself uses quotes.
I tried glancing through here and here, but couldn't spot the notation definition.
Couldn't figure out how to use the
Locate command properly for that either.. :grimacing:
But there is no way to escape the quotes, is there?
Require Import String. Check "hello"%string. Check """"%string.
I believe that the second string is one quote symbol (escaped), but I will search for definite answer in documentation.
That does seem to be a single quote (
It comes down to
(Ascii.Ascii false true false false false true false false)
which is for
I guess there's some rule that I'm yet to find out.
Locate " """" """" "%string. (* Unknown notation *)
to find the definition of the string notation didn't work.
I thought maybe
"""" can be used instead of
" here. I guess not.
I don't think you can look it up, it's not definable with the
from the last time I looked, I think string notations are a plugin, so defined at the OCaml level (where one can in principle come up with any crazy syntax)
I couldn't understand much of it, but is this that plugin?
yes, that's one of the source files. The interface between OCaml and Coq is here.
And how was
" 'escaped' (not sure if that' the right word :sweat_smile: ) in
Can we escape other characters as well using something similar? Like newline (
a plugin can directly hook into Coq's parser and lexer, so it can do that, sure
Ju-sh has marked this topic as resolved.
It's no longer OCaml defined for quite some time, look for
String Notation (both in the manual and in
@Pierre Roux Is this same as the
String Notation mentioned here? https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#string-notations
And what could the stuff here be doing? Is it for implementing
String Notation syntax itself or something?
yes and yes
Last updated: Feb 09 2023 at 00:03 UTC