1
votes

I mean the list symbol in case it does not show up well in the title.

It is not \bl like the book says.

4
Have you put the code from the "Some Extra Emacs Definitions" section in your .emacs file?Anton Trunov
Yeah, this is what I need. Only the copy/paste eats the newlines, so it would not be bad if somebody provided the definitions in text rather than pdf. I'll try to find it myself.Marko Grdinić

4 Answers

1
votes

The book provides the code to make typing easier in the "Some Extra Emacs Definitions" addendum:

(eval-after-load "quail/latin-ltx"
   '(mapc (lambda (pair)
            (quail-defrule (car pair) (cadr pair) "TeX"))
           '( ("\\bb" "𝔹") ("\\bl" "𝕃") ("\\bs" "𝕊") ("\\bt" "𝕋") ("\\bv" "𝕍") ("\\cv" "⋎") ("\\comp" "○") ("\\m" "↦") ("\\om" "ω"))))

You just need to copy it from here and paste it into your .emacs file.

1
votes

It's not part of the emacs mode yet but I have submitted a Pull Request to add the missing blackboard bold letters.

0
votes

Use M-x then agda-input-show-translations get a table of all the character bindings. Then you can use C-s to search for a specific character.

0
votes

In my case I just typed in Emacs

\bL 

, which gives me the blackboard bold font correctly. This is with agda 2.5.3 (installed via hackage per official documentation under Ubuntu 16.04)