[Agda] Font questions again

Martin Escardo m.escardo at cs.bham.ac.uk
Fri Dec 22 21:33:13 CET 2017


I want to use the powerset symbol, which is \MCP (calligraphic capital
P).

If I do agda-input-show-translations, then I get to see this symbol
properly rendered, saying that it should be typed as \MCP.

However, when I use \MCP in an agda file, the symbol is not rendered
(by the same emacs session) and I instead see a square with a matrix
of hexadecimal numbers inside it.

Let me try it here to see what the message is displayed like: 𝓟.

I have

    (set-fontset-font "fontset-default" 'unicode "DejaVu Sans")

in my .emacs as suggested here in this list some time ago (I think by
Paolo Capriotti), which works for many symbols, but not this.

Why can emacs display it in the agda-input-show-translations buffer,
but not in my agda buffer? Any clues?

Thanks,
Martin


More information about the Agda mailing list