Unicode Input

How can I write Unicode characters using Emacs?

The Agda Emacs mode turns on a special input method which enables you to type many symbols. This input method is highly customisable (via M-x customize-group agda-input). By default you can insert a number of symbols by typing their TeX/LaTeX names. For instance, if you type \forall then ∀ gets inserted. Some characters have key bindings which have not been taken from LaTeX (typing \bn results in ℕ being inserted, for instance), but all bindings start with \.

Type M-x agda-input-show-translations RET RET to see all the characters you can type using this input method (with some exceptions in certain versions of Emacs).

If you know the Unicode name of a character you can also use ucs-insert (which supports tab-completion). Example:

  C-x 8 RET not SPACE a SPACE sub TAB RET

inserts the character “NOT A SUBSET OF” (⊄). You can use M-x ucs-insert RET instead of C-x 8 RET if you want to.

(The Agda input method has one drawback: if you make a mistake while typing the name of a character, then you need to start all over again. If you find this terribly annoying, then you can use Abbrev mode instead. However, note that Abbrev mode cannot be used in the minibuffer, which is used to give input to many Agda and Emacs commands.)

OK, but how can I find out what to type to get the character?

To find out how to write a given character which is already present in an Emacs buffer, do the following:

Position the cursor over the character and press C-u C-x =. For instance, for ∷ I get the following:

     character: ∷ (343127, #o1236127, #x53c57, U+2237)
       charset: mule-unicode-0100–24ff (Unicode characters of the range U+0100..U+24FF.)
    code point: #x78 #x57
        syntax: w 	which means: word
      to input: type “\::” with Agda
   buffer code: #x9C #xF4 #xF8 #xD7
     file code: #xE2 #x88 #xB7 (encoded by coding system mule-utf-8-unix)
       display: by this font (glyph code)
        -Misc-Fixed-Medium-R-Normal—15–140–75–75-C-90-ISO10646–1 (#x2237)

Here it says that I can type \:: to get a ∷. If there is no “to input” line, then you can add a key binding to the Agda input method by using M-x customize-variable agda-input-user-translations.

Show me some commonly used characters

Some characters which are commonly used in the standard library can be typed as follows:

CharacterShort key bindingLaTeX-like key binding
\r-\to
\_1 
\_2 
\~~\approx
\all\forall
\> 
\< 
 \ell
\==\equiv
\~\sim
\<=\le
\’1\prime
\:: 
λ\Gl\lambda
 \neg
\o\circ
\bn\Bbb{N}
\x\times

Howto