[Agda] Disappearing unicode in Literate Agda - XeLatex

[Andrés Sicard-Ramírez]

On 30 December 2017 at 14:39, Matthew Daggitt <matthewdaggitt at gmail.com> wrote:
> I am getting slightly different symptoms as I'm getting no errors at all in
> the log, so there is no
>
>   Missing character: There is no ℕ in font cmss10!
>
> error appearing. My code.lagda file is as follows:
>
>   \documentclass{article}
>
>   \usepackage{agda}
>
>
>   \begin{document}
>
>
>   \begin{code}
>
>       data ℕ : Set where
>
>   \end{code}
>
>
>   \end{document}
>
>
> My tex version is:
>
>   XeTeX 3.14159265-2.6-0.99992 (TeX Live 2015/Debian)
>   kpathsea version 6.2.1
>

Using the same version of XeLaTeX (but not installed via Debian)

  $ xelatex --version
  XeTeX 3.14159265-2.6-0.99992 (TeX Live 2015)
  kpathsea version 6.2.1

I see the missing character warning:

$ grep Missing code.log
Missing character: There is no ℕ in font cmss10!
Missing character: There is no ℕ in font cmss10!
Missing character: There is no ℕ in font cmss10!

--
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.