agda/test/LaTeXAndHTML/succeed/Multiline.quick.tex

\documentclass{article}
\usepackage{agda}
\begin{document}
\begin{code}%
\>[0]\AgdaKeyword{open}\AgdaSpace{}%
\AgdaKeyword{import}\AgdaSpace{}%
\AgdaModule{Agda.Builtin.String}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{argh}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPostulate{String}\<%
\\
\>[0]\AgdaFunction{argh}\AgdaSpace{}%
\AgdaSymbol{=}%
\>[8]\AgdaString{"Hello,\textbackslash{}}\<%
\\
%
\>[8]\AgdaString{\textbackslash{}World!"}\<%
\end{code}
\end{document}