Stream: Coq users

Topic: ✔ Is quote in string 'escaped'?


view this post on Zulip Julin S (Jan 08 2022 at 17:34):

In an earlier discussion here, I found out about

Compute """"%string.  (* string with a single character of double quote *)

It looks as if a double quote was 'escaped' or something. What is really happening here?

And are there other characters which can be escaped like this?

view this post on Zulip Li-yao (Jan 08 2022 at 18:05):

Two double quotes is how you escape a double quote in a string, and apart from that all other bytes are read literally until the closing double quote.

view this post on Zulip Julin S (Jan 08 2022 at 18:28):

Okay, so a "" stands for a single double quote and we can write ab"cd"ef like

Compute "ab""cd""ef"%string.

Thanks!

view this post on Zulip Notification Bot (Jan 08 2022 at 18:28):

Julin S has marked this topic as resolved.

view this post on Zulip Gaëtan Gilbert (Jan 08 2022 at 18:50):

why use Compute?

view this post on Zulip Julin S (Jan 08 2022 at 19:12):

Just as a way to make the string appear in the info output. Is there another way?

view this post on Zulip Gaëtan Gilbert (Jan 08 2022 at 19:14):

Check

view this post on Zulip Gaëtan Gilbert (Jan 08 2022 at 19:15):

also you probably don't need %string


Last updated: Feb 01 2023 at 13:03 UTC