[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