[Agda] Disappearing unicode in Literate Agda - XeLatex

[Nils Anders Danielsson]

On 2017-12-30 14:47, Matthew Daggitt wrote:
> 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.

This is a known problem:

   LaTeX backend + XeLaTeX/LuaLaTeX ⇒ no lambda
   https://github.com/agda/agda/issues/2225

I assume that the output from XeLaTeX includes something like the
following:

   Missing character: There is no ℕ in font cmss10!

This can be handled in different ways. I've used newunicodechar, but
this solution does not play well together with microtype, which is used
by acmart. For my latest paper I decided to use pdfLaTeX instead. (I
used \DeclareUnicodeCharacter, and gave the nofontsetup and
noinputencodingsetup options to agda.sty.)

-- 
/NAD