agda/test/LaTeXAndHTML/succeed/TeXExtension.lagda.tex

\documentclass{article}
\usepackage{agda}

\begin{document}

Foo

\begin{code}

module TeXExtension where

  data Bool : Set where
    true : Bool
    false : Bool

  b : Bool
  b = false

\end{code}

  c : Bool
  c = broccoli

\end{document}