[Agda] Disappearing unicode in Literate Agda - XeLatex

[Matthew Daggitt]

I've been trying to get literate agda up and running as per the
instructions in the documentation
<https://agda.readthedocs.io/en/v2.5.3/tools/generating-latex.html>
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171230/ab6878d2/attachment.html>