[Agda] how to count 0..n-1

[Nils Anders Danielsson]

On 2011-02-18 10:06, Dominique Devriese wrote:
> 2011/2/18 Jason Dusek<jason.dusek at gmail.com>:
>>   The interaction between the '\le' shortcut and the letter 'n' is
>>   most unfortunate.
>
> In the emacs input mode, you mean? If so, I completely agree :)

You can remove bindings which you do not like by using
M-x customize-group agda-input.

> Emacs also doesn't let you use the agda input mode in the interactive
> search, which is very annoying.

Yes it does, at least under Emacs 23.2.1. From the help message for C-s:

   "If an input method is turned on in the current buffer, that input
   method is also active while you are typing characters to search. To
   toggle the input method, type C-\. It also toggles the input method in
   the current buffer."

-- 
/NAD