[Agda] Lambda

[Anton Setzer]

Nils Anders Danielsson wrote:
> On Wed, Jun 18, 2008 at 6:43 PM, Anton Setzer <A.G.Setzer at swansea.ac.uk> wrote:
>   
>> There is an easy way of using such symbols (and other
>> special symbols) by using the abbreviation mode.
>>     
>
> Yes, I have documented this as one possible way forward:
>
>   http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Docs.UnicodeInput
>   (Last section.)
>
> However, I would not say that it is easy. Someone has to compile a
> table of "abbreviations", and this can involve quite a lot of work,
> especially if we want to have a good, consistent naming convention.
>
> So, do we really want to construct and maintain a special input method
> for Agda, instead of using out-of-the-box solutions? The
> out-of-the-box solutions are not optimal, but designing our own one
> requires work, and increases fragmentation on the input method scene.
>
> On balance I think that it could be a good idea to design our own
> method, but someone needs to do the work. One approach is for someone
> to come up with a good (tested) naming convention, and then we can
> expand the initial "abbreviation" tables collaboratively, perhaps
> through the Agda wiki.
>
>   
I have been using abbrev mode for a long time when editing latex documents,
because the backslash key is so difficult to reach. So in latex my
convention
is that the abbreviation consists of omitting the backslash and doubling
the last character.
   (there are exceptions, when with doubling the last character one
obtains something
    which is typed occasionally on its own - but in most cases one comes
up with an
    abbreviation which one wouldn't use as a symbol).
That would solve the problem for most latex-like abbreviations, which
are I assume the
 ones we use most often.

Here are by the way my agda2 abbreviations which work very well (but
there are very few;
note the use of arr for -> which makes typing of arrows fast):

(agda2-mode-abbrev-table)

"bott"           2    "⊥"
"topp"           9    "⊤"
"lorr"           3    "∨"
"nbbb"           23   "ℕ"
"arr"           15   "->"

Anton

> Another option is to improve the standard Emacs input methods, but
> given the slow release cycle of Emacs this seems like a bad idea. Does
> anyone know if there are any non-Emacs-specific input methods which
> handle Unicode symbols? (Not counting the methods of clicking in a
> character table or entering code points manually.)
>
>   
>> By the way, a list of symbols usable in leim
>> can be found here:
>>
>> http://www.cs.swan.ac.uk/~csetzer/othersoftware/agda2/leimListOfSymbols.txt
>>     
>
> Note that we cannot simply steal this list (and then modify it
> according to our circumstances); LEIM is GPL-ed, so we would get
> licensing issues.
>
>   


-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------
 
                    
  

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080619/c158fe34/attachment.html