Backslash characters `\` are interpreted as escape characters when printed to the agda view

banacorn / agda-mode-vscode

agda-mode on VS Code

MIT License

167 stars 38 forks source link

Open fredrik-bakke opened 6 months ago

fredrik-bakke commented 6 months ago

Minimal reproducing example

a = {! b\nc !}

Using C-c C-n, one gets