The Coq mailing list

[Chantal Keller <chantal.keller AT wanadoo.fr>]

Hi,

You can use the package ucs [1], declare unicode characters (here is an
example for λ) that way:

\DeclareUnicodeCharacter{955}{\ensuremath{\lambda}}

and then use unicode symbols inside LaTeX as well as in listings.

The package ucs seems not to be maintained anymore, but it works well.

Hope this helps,

Chantal.

[1] http://www.unruh.de/DniQ/latex/unicode

Le 26/05/2010 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
> 
>