Non-visible ASCII codes inside of a String

Stream: new members

[Luis Enrique Muñoz Martín]

Hi, I wanted to know how I can write ascii codes inside of a string.

i.e. the ESC ascii code is represented as \x1b is most languages (number 27). In those languages I can easy embed that into a string: "ESC code: \x1b".

Nevertheless the closest I can get in lean is as follows:

#eval s!"ESC code: {Char.ofNat 0x1B}" -- ESC code: \x1b

Which is super verbose if I want to use several codes in the same string. Is there any shortcut for this? I'm not able to find information about this in the Lean Manual.

[Kyle Miller]

It doesn't seem to appear in the online manual, but in the sources there's a file on lexical structure: https://github.com/leanprover/lean4/blob/master/doc/lexical_structure.md#string-literals

[Kyle Miller]

This works for me:

#eval s!"ESC code: \x1b"

What problem are you running into?

[Luis Enrique Muñoz Martín]

Ouch! That's true. My fault. My IDE was changing slightly the character after writting \x :face_palm:

Thanks!!

[Kyle Miller]

It took me awhile to get used to needing to type \\ for a \ in VS Code (and I'm not sure I've fully gotten used to it)

[Kevin Buzzard]

Oh wow! I would always type the x1b first and then go back and add the \ afterwards :-)

[Mario Carneiro]

I usually just let it complete, then undo