agda/test/LaTeXAndHTML/succeed/TeXExtension.tex

\documentclass{article}
\usepackage{agda}

\begin{document}

Foo

\begin{code}%
\>[0]\<%
\\
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{TeXExtension}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{Bool}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaInductiveConstructor{true}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
%
\>[4]\AgdaInductiveConstructor{false}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
%
\>[2]\AgdaFunction{b}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
%
\>[2]\AgdaFunction{b}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{false}\<%
\\
\>[0]\<%
\end{code}

  c : Bool
  c = broccoli

\end{document}