The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

Thanks for the hint, we got this method to work. Meanwhile, I see it
has also been documented in svn.


While playing with it I wonder what restrictions Coq has for the use of 
unicode.
It seems that we can only use letter-like symbols in Definitions.
Wouldn't it be nice to allow more general symbols.
E.g. to allow â—Ž as the name for a function without poluting the name
space by first defining
Definition my_long_function_name :nat->nat->nat:= ...
Notation "n â—Ž m" ...

??

Bas

2010/2/17 Pierre-Marie Pédrot 
<pierremarie.pedrot AT ens-lyon.fr>:
> Pierre Courtieu wrote:
>> for coqide the only method I know of is the one explained in the coq
>> reference manual:
>>
>> http://coq.inria.fr/coq/refman/Reference-Manual019.html#toc106
>
> For coqide, as it uses GTK, you could also use any input method editor
> (such as scim or ibus) and write a m17n file describing the input you
> wish to have (e.g. mimic the one of Emacs).
>
> This language is very rich, and you can have its description here :
> http://www.m17n.org/common/m17n-docs-en/m17nDBFormat.html#mdbIM
>
> For a simpler insight, one can have a look into basic mim files
> (eo-plena.mim is a good start).
>
> I don't know how it is described in Emacs, but it should be similar, and
> translation should be easy. If someone is interested, I may try to write
> it myself, as long as I have the bindings.
>
> PMP
>
>