<div dir="ltr"><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap"><span style="font-family:arial,helvetica,sans-serif">I've been trying to get literate agda up and running as per the instructions in the <a href="https://agda.readthedocs.io/en/v2.5.3/tools/generating-latex.html">documentation</a> 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 .</span></pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap"> </pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \documentclass{article}</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap"> </pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \usepackage{agda}</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap"> </pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \begin{document}</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap"> </pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  ℕ</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap"> </pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \begin{code}%</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  %</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \>[4]\AgdaKeyword{data}\AgdaSpace{}%</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \AgdaDatatype{ℕ}\AgdaSpace{}%</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \AgdaSymbol{:}\AgdaSpace{}%</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \AgdaPrimitiveType{Set}\AgdaSpace{}%</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \AgdaKeyword{where}\<%</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \end{code}</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap"> </pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">   \end{document}</pre><p style="color:rgb(0,0,0)"><font face="Lucida Grande, Verdana, Arial, Helvetica, sans-serif" style="font-size:13.3333px">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. </font><span style="white-space:pre-wrap"><font face="arial, helvetica, sans-serif" style="">The same problem occurs when I place any unicode character inside the \AgdaDatatype{} command. </font></span><span style="font-size:13.3333px;font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif">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):</span></p><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \usepackage{bbm}</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \usepackage[greek,english]{babel}<br></pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \usepackage{ucs}</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \usepackage[utf8x]{inputenc}</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">  \usepackage{autofe}<br><br>Does anyone have any suggestions?</pre><pre style="color:rgb(0,0,0);font-family:"Lucida Grande",Verdana,Arial,Helvetica,sans-serif;font-size:12px;margin-top:0px;margin-bottom:0px;padding:0px;word-wrap:break-word;white-space:pre-wrap">Thanks,<br>Matthew</pre></div>