[Agda] Unicode
Harley D. Eades III
harley.eades at gmail.com
Fri Jan 31 18:25:10 CET 2014
Hi, Nils.
On Jan 31, 2014, at 4:52 AM, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> On 2014-01-31 00:01, Harley Eades wrote:
>> I am using Mac OS X, and standard Emacs 24.3, and unicode with Agda is
>> pretty well supported on my system, but the only blackboard-bold
>> characters I have are \bn, \br, \bp, and \bz, but I want would like to
>> have \Bbb{B}. Does anyone have this working on their system?
>
> On my system 𝔹 is displayed using the FreeSerif font (according to
> C-u C-x =).
Did you have to do anything special getting the font to work?
I found that this can be downloaded from
http://ftp.gnu.org/gnu/freefont/, however I can't seem to get Mac OS X
to like the fonts.
Thanks for your help.
.\ Harley
>
> --
> /NAD
>
More information about the Agda
mailing list