[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