\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}