[Agda] help with math symbols

[Jean-Philippe Bernardy]

>
>
> d) With this,  emacs  still shows correctly specific math symbols
>    in the  .adga  files,
> but I cannot correctly _input_ these math symbols. For example,
> my program
>           open import Nat
>           ...
>           f : \bn
>           f = zero
> does not compile, the compiler takes  \bn  as lambda.
>
> Please, how to fix the setting?
>
>
You need to activate the Agda input method. For example:

M-x set-input-method

and type Agda at the prompt.

Another useful shortcut to know is C-\
(Use M-x describe-key C-\ for the doc.)

Cheers,
JP.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120730/0a993fbc/attachment.html