[Agda] help with math symbols

Serge D. Mechveliani mechvel at botik.ru
Mon Jul 30 12:30:43 CEST 2012


On Mon, Jul 30, 2012 at 12:10:55PM +0200, Jean-Philippe Bernardy wrote:
> >
> >
> > 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.

I type it, and obtain

  Select input method (default russian-computer): Agda
 
and press RETURN.
It responds (in the same line)  "no match".
The same is for `agda'.

------
Sergei


More information about the Agda mailing list