[Agda] Agda pragmas are rendered incorrectly in lhs2tex

Andrés Sicard-Ramírez andres.sicard.ramirez at gmail.com
Sat Oct 20 18:06:04 CEST 2012


Hi Andreas,

On Sat, Oct 20, 2012 at 3:01 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Hi Andres,
>
> I used
>
> %% BEGIN WORKAROUND lhs2TeX
> \hide{
> \begin{code}
> {-# NO_TERMINATION_CHECK #-}
> \end{code}
> }
> \begin{verbatim}
>     {-# NO_TERMINATION_CHECK #-}
> \end{verbatim}
> %% END
>

Thanks, it solved my issue.

Best,

-- 
Andrés


More information about the Agda mailing list