<div dir="ltr">Thank you very much for the link to the issue. I'm only trying to typeset a small amount so the \newunicodechar workaround is fine for now. It might be worth splicing it into the documentation as it seems it's been open for a while. <div><br></div><div>I am getting slightly different symptoms as I'm getting no errors at all in the log, so there is no</div><div><br style="font-size:12.8px"><span style="font-size:12.8px"> Missing character: There is no ℕ in font cmss10!</span><br></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">error appearing. My code.lagda file is as follows:</span></div><div><span style="font-size:12.8px"><br></span></div><div>
<pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(128,0,0)"> \documentclass</span><span style="color:rgb(0,0,0)">{article}</span></pre>
<pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(128,0,0)"> \usepackage</span><span style="color:rgb(0,0,0)">{agda}</span></pre>
<pre style="margin-top:0px;margin-bottom:0px"><br></pre>
<pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,204)"> \begin</span><span style="color:rgb(0,0,0)">{document}</span></pre>
<pre style="margin-top:0px;margin-bottom:0px"><br></pre>
<pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,204)"> \begin</span><span style="color:rgb(0,0,0)">{code}</span></pre>
<pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,0)"> data ℕ : Set where</span></pre>
<pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,204)"> \end</span><span style="color:rgb(0,0,0)">{code}</span></pre>
<pre style="margin-top:0px;margin-bottom:0px"><br></pre>
<pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,204)"> \end</span><span style="color:rgb(0,0,0)">{document}</span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,0)"><br></span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,0)"><font face="arial, helvetica, sans-serif">And my code.tex is file is:</font></span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,0)"><br></span></pre><pre style="margin-top:0px;margin-bottom:0px"><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(128,0,0)"> \documentclass</span><span style="color:rgb(0,0,0)">{article}</span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(128,0,0)"> \usepackage</span><span style="color:rgb(0,0,0)">{agda}</span></pre>
<pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,204)"> \begin</span><span style="color:rgb(0,0,0)">{document}</span></pre>
<pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,204)"> \begin</span><span style="color:rgb(0,0,0)">{code}</span><span style="color:rgb(96,96,96)">%</span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(96,96,96)"> %</span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(128,0,0)"> \></span><span style="color:rgb(0,0,0)">[4]</span><span style="color:rgb(128,0,0)">\AgdaKeyword</span><span style="color:rgb(0,0,0)">{data}</span><span style="color:rgb(128,0,0)">\AgdaSpace</span><span style="color:rgb(0,0,0)">{}</span><span style="color:rgb(96,96,96)">%</span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(128,0,0)"> \AgdaDatatype</span><span style="color:rgb(0,0,0)">{λ}</span><span style="color:rgb(128,0,0)">\AgdaSpace</span><span style="color:rgb(0,0,0)">{}</span><span style="color:rgb(96,96,96)">%</span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(128,0,0)"> \AgdaSymbol</span><span style="color:rgb(0,0,0)">{:}</span><span style="color:rgb(128,0,0)">\AgdaSpace</span><span style="color:rgb(0,0,0)">{}</span><span style="color:rgb(96,96,96)">%</span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(128,0,0)"> \AgdaPrimitiveType</span><span style="color:rgb(0,0,0)">{Set}</span><span style="color:rgb(128,0,0)">\AgdaSpace</span><span style="color:rgb(0,0,0)">{}</span><span style="color:rgb(96,96,96)">%</span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(128,0,0)"> \AgdaKeyword</span><span style="color:rgb(0,0,0)">{where}</span><span style="color:rgb(128,0,0)">\<</span><span style="color:rgb(96,96,96)">%</span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,204)"> \end</span><span style="color:rgb(0,0,0)">{code}</span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,0)"><br></span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,204)"> \end</span><span style="color:rgb(0,0,0)">{document}</span></pre><pre style="margin-top:0px;margin-bottom:0px"><span style="color:rgb(0,0,0)"><br></span></pre><pre style="margin-top:0px;margin-bottom:0px"><font color="#000000"><font face="arial, helvetica, sans-serif">My tex version is:
</font><br></font></pre><pre style="margin-top:0px;margin-bottom:0px"><font color="#000000"> XeTeX 3.14159265-2.6-0.99992 (TeX Live 2015/Debian)
kpathsea version 6.2.1
</font></pre></pre></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Dec 30, 2017 at 5:15 PM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 2017-12-30 14:47, Matthew Daggitt wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
When I compile it using XeLatex (or LuaLatex) everything compiles<br>
without errors and it all appears fine (including the first ℕ symbol<br>
outside of the code block) except that the ℕ symbol inside the<br>
\AgdaDatatype{} command doesn't appear.<br>
</blockquote>
<br></span>
This is a known problem:<br>
<br>
LaTeX backend + XeLaTeX/LuaLaTeX ⇒ no lambda<br>
<a href="https://github.com/agda/agda/issues/2225" rel="noreferrer" target="_blank">https://github.com/agda/agda/i<wbr>ssues/2225</a><br>
<br>
I assume that the output from XeLaTeX includes something like the<br>
following:<br>
<br>
Missing character: There is no ℕ in font cmss10!<br>
<br>
This can be handled in different ways. I've used newunicodechar, but<br>
this solution does not play well together with microtype, which is used<br>
by acmart. For my latest paper I decided to use pdfLaTeX instead. (I<br>
used \DeclareUnicodeCharacter, and gave the nofontsetup and<br>
noinputencodingsetup options to agda.sty.)<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br></div>