[Agda] Disappearing unicode in Literate Agda - XeLatex

[Andrés Sicard-Ramírez]

Agda, XeLaTeX and LuaLaTeX versions?

Also attach `code.lagda` please.


On 30 December 2017 at 08:47, Matthew Daggitt <matthewdaggitt at gmail.com> wrote:
> I've been trying to get literate agda up and running as per the instructions
> in the documentation and I'm having problems getting unicode symbols to
> appear inside code blocks. I've run "agda --latex code.lagda" to get the
> following "code.tex" file below .
>
>
>
>   \documentclass{article}
>
>
>
>   \usepackage{agda}
>
>
>
>   \begin{document}
>
>
>
>   ℕ
>
>
>
>   \begin{code}%
>
>   %
>
>   \>[4]\AgdaKeyword{data}\AgdaSpace{}%
>
>   \AgdaDatatype{ℕ}\AgdaSpace{}%
>
>   \AgdaSymbol{:}\AgdaSpace{}%
>
>   \AgdaPrimitiveType{Set}\AgdaSpace{}%
>
>   \AgdaKeyword{where}\<%
>
>   \end{code}
>
>
>
>    \end{document}
>
> When I compile it using XeLatex (or LuaLatex) everything compiles without
> errors and it all appears fine (including the first ℕ symbol outside of the
> code block) except that the ℕ symbol inside the \AgdaDatatype{} command
> doesn't appear. The same problem occurs when I place any unicode character
> inside the \AgdaDatatype{} command. I've tried adding in various
> combinations of the following package imports (even though according to the
> documentation they shouldn't be necessary in XeLatex):
>
>   \usepackage{bbm}
>
>   \usepackage[greek,english]{babel}
>
>   \usepackage{ucs}
>
>   \usepackage[utf8x]{inputenc}
>
>   \usepackage{autofe}
>
> Does anyone have any suggestions?
>
> Thanks,
> Matthew
>
> La información contenida en este correo electrónico está dirigida únicamente
> a su destinatario y puede contener información confidencial, material
> privilegiado o información protegida por derecho de autor. Está prohibida
> cualquier copia, utilización, indebida retención, modificación, difusión,
> distribución o reproducción total o parcial. Si usted recibe este mensaje
> por error, por favor contacte al remitente y elimínelo. La información aquí
> contenida es responsabilidad exclusiva de su remitente por lo tanto la
> Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The
> information contained in this email is addressed to its recipient only and
> may contain confidential information, privileged material or information
> protected by copyright. Its prohibited any copy, use, improper retention,
> modification, dissemination, distribution or total or partial reproduction.
> If you receive this message by error, please contact the sender and delete
> it. The information contained herein is the sole responsibility of the
> sender therefore Universidad EAFIT is not responsible for what the message
> contains.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.