[Agda] Agda pragmas are rendered incorrectly in lhs2tex

[Andreas Abel]

Hi Andres,

I used

%% BEGIN WORKAROUND lhs2TeX
\hide{
\begin{code}
{-# NO_TERMINATION_CHECK #-}
\end{code}
}
\begin{verbatim}
     {-# NO_TERMINATION_CHECK #-}
\end{verbatim}
%% END

with the obvious definition of \hide.

Not pretty, but better than funny subscripts.

Cheers,
Andreas

On 19.10.12 5:35 PM, Andrés Sicard-Ramírez wrote:
> Hi,
>
> Andreas reported that lhs2tex render a pragma like
>
> {-# NO_TERMINATION_CHECK #-}
>
> in math mode, i.e. interpreting _ as subscript
>
> (see https://github.com/kosmikus/lhs2tex/issues/18 )
>
> Anyone know a solution for this issue?
>
> Thanks,
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/