\documentclass{article} \usepackage{agda} \begin{document} \begin{code} open import Agda.Builtin.String argh : String argh = "Hello,\ \World!" \end{code} \end{document}