[Agda] Lambda

Anton Setzer A.G.Setzer at swansea.ac.uk
Wed Jun 18 19:43:58 CEST 2008


Concerning using \lambda instead of \:

There is an easy way of using such symbols (and other
special symbols) by using the abbreviation mode.

http://www.cs.swan.ac.uk/~csetzer/othersoftware/agda2/agdainstallAbbreviationMode.pdf
contains instructions how to use it.

Before I was using abbreviation mode I was avoiding special symbols.
With the abbreviation mode it has become fun to use them (only searching)
is a bit tricky).

So if one gave some predefined definitions in abbrev-mode
such as lamm for the symbol representing lambda and
arr for the symbol representing an arrow, it could be fairly
easy to use.

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



Anton

-- 
---------------------------------------
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/
---------------------------------------
 
                    
  



More information about the Agda mailing list