1

I try to to make agda code using unicode characters such as greek characters readable in a LaTeX2e file (which uses a lmcs.cls file http://www.lmcs-online.org/Information/lmcs.cls ). So, I cannot use XeLaTeX instead as recommended to similar problem.

More precisely I added the necessary lines from http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda to my file. As described there, it can happen that certain unicode characters are still not yet available and need to be declared separately.

Here is a (possibly minimal) example:

 \documentclass{lmcs}

\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{autofe}

\usepackage[greek,english]{babel} %note: after loading autofe

\DeclareUnicodeCharacter{"03B9}{\textiota}     % ι
\DeclareUnicodeCharacter{"27E6}{\llbracket} 

\begin{document}
ι
⟦
\end{document}

The problems with this are: 1)even if there is no error message, \textiota is not displayed in the pdf output, 2) there is an error message Undefined control sequence. \u-document-10214 #1->\llbracket

  • 1
    Note that there's a difference between the example code and what is suggested: \DeclareUnicodeCharacter{"03B9}{\textiota} - note the use of ". – Werner Feb 24 '17 at 1:17
  • Thanks for your answer. Sorry, where is the " suggested? When I add it, I still receive the same error message. – guest Feb 24 '17 at 1:26
  • It is in the syntax given on the page you linked to. If you still get an error, post a proper minimal example we can compile to reproduce the error. Please also provide the exact text of the error message and not just a summary or interpretation. – cfr Feb 24 '17 at 4:23
  • 1
    @cfr @Werner The linked page suggests ! The correct character is ". – Paul Gaborit Feb 24 '17 at 6:06
  • 2
    @Werner The linked page suggests \DeclareUnicodeCharacter{”03B9}{\textiota} instead of \DeclareUnicodeCharacter{"03B9}{\textiota} (note the difference between and "). – Paul Gaborit Feb 25 '17 at 6:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.