☰

如何设置 Agda 代码使用的字体？

tag-icon • tag-icon fonts
如何设置 Agda 代码使用的字体？

我正在关注此处的文档： https://agda.readthedocs.io/en/v2.6.0.1/tools/generating-latex.html

由此，我想出了以下例子

\documentclass{article}

\usepackage{agda}

\usepackage{fontspec,unicode-math}
\setmainfont{XITS}
\setmathfont{XITS Math}

\begin{document}

ℕ

\begin{code}

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

\end{code}

\end{document}

但是，当我使用

agda --latex example.lagda
xelatex example.tex

第一个 ℕ 字符在 PDF 中显示正常，但代码环境中的 ℕ 却没有。当我查看 xelatex 日志时，我看到

Missing character: There is no ℕ in font [lmsans10-regular]:mapping=tex-text;!

对我来说，这意味着它没有在主字体或数学字体中寻找 ℕ 字符。有没有办法指定代码环境要使用的字体？

agda --latex example.lagda可以在以下位置找到通过命令生成的 latexhttps://pastebin.com/6gBw51Jb。

答案1

我没有 agda.sty 并且不会尝试去寻找它，但它看起来好像使用无衬线字体，所以你可以尝试一下\setsansfont{XITS}。

相关内容