Skip to content

Instantly share code, notes, and snippets.

@gallais
Created November 18, 2013 15:16
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save gallais/7529438 to your computer and use it in GitHub Desktop.
Underscore in a pragma breaks the lhs2tex-generated LaTeX code
\documentclass{article}
%include lhs2TeX.fmt
%include lhs2TeX.sty
%include polycode.fmt
\begin{document}
\begin{code}
module Equal where
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
\end{code}
\end{document}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment