I'm trying to play around with coq-parsec: https://github.com/liyishuai/coq-parsec
In particular, I'm trying to write code like the following:
Example parseLFExample : parse parseLF "\n" = inr ("010"%char, ""). Proof. unfold parse. simpl. reflexivity. Qed.
The call to
reflexivity gives a message like the following:
Unable to unify "inr ("010"%char, "")" with "inl (Some (String "D" (String "i" (String " ...
My guess is that
"\n" is not a legal way in Coq to write a string with a single newline character (possibly because coq doesn't know about newline escape sequences?). How would I write a string in Coq with a newline in it? For instance, in Haskell I could write something like
Relatedly, how would I write a multi-line string in Coq? For instance, in Haskell, You can't naively write:
myString :: String myString = "hello this is a multiline string"
(Although there are various ways of working around this limitation and getting something similar to this to work....)
How would you do something like this in Coq?
Not sure if this is exactly what you need, but for writing multiline strings, I tried
Compute "hi hello"%string (* = "hi hello"%string : string *)
and the new line is showing coming up as part of the string.
@Julin S Thanks! So I guess if I want to write a string with a newline, I can just literally write a string that spans over multiple lines.
Although I'm wondering why you are using
%string here. Is there a difference between
"hello"%string in Coq?
It's to mention the scope for the notation. To use the notation (placing characters inside
" ") to enter strings in user friendly way.
I think this is the relevant docs: https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#notation-scopes
Strings are really represented using
The notation allows us to write
String (Ascii true false false false false false true false) EmptyString
But %string is usually not necessary
(depending on your scope setup, of course)
Ah okay, thanks. That makes sense.
Last updated: Jan 27 2023 at 00:03 UTC