The Coq mailing list

[David Pichardie <David.Pichardie AT inria.fr>]

Hi,

During my short experience with listings and utf8, it has been  
necessary to replace on the fly all utf8 symbol with the following  
LaTeX command.

\lstset{literate={forall}{{$\forall$}}1%
{->}{{$\mathtt{\to}$}}1%
{ρ}{{$\mathtt{\rho}$}}1%
{∧}{{$\land$}}1%
{∀}{{$\forall$}}1%
{⊔}{{$\sqcup$}}1%
{⊥}{{$\bot$}}1%
{⊤}{{$\top$}}1%
{<<}{{$\langle$}}1%
{>>}{{$\rangle$}}1%
{↦}{{$\mapsto$}}1%
{∃}{{$\exists$}}1%
{℘}{{$\mathcal{P}$}}1%
{⊓}{{$\sqcap$}}1
{γ}{{$\gamma$}}1
{○}{{$\circ$}}1
{♯}{{$^\sharp$}}1
{⊑}{{$\sqsubseteq$}}1}

Hope this helps.

David.


Le 26 mai 10 à 14:07, Bas Spitters a écrit :

> Many Coq-users use the latex listings environment for Coq-commands.
> http://www.ctan.org/tex-archive/macros/latex/contrib/listings/
>
> Is there any experience using this with unicode symbols?
>
> Thanks,
>
> Bas