Stream: Coq users

Topic: ✔ Is quote in string 'escaped'?

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?

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.

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!

Notification Bot (Jan 08 2022 at 18:28):

Julin S has marked this topic as resolved.

Gaëtan Gilbert (Jan 08 2022 at 18:50):

why use Compute?

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?

Gaëtan Gilbert (Jan 08 2022 at 19:14):

Check

Gaëtan Gilbert (Jan 08 2022 at 19:15):

also you probably don't need %string

Last updated: Oct 13 2024 at 01:02 UTC