Here follow brief instructions on how to start Agda in the Linux lab
in the CS departement at Swansea University:


Edit the file ~/.bashrc  (if this file doesn't exist create it)
and add the lines

agda2localpath=/compsci/saturn/staff/csetzer/agda2/programsused/local/bin/
export PATH=${agda2localpath}:${PATH}


Edit  the file ~/.emacs (if this file doesn't exist create it)
and add the lines

(load "/compsci/saturn/staff/csetzer/emacs/agdainstall")



Start a new shell or console. This will activate evaluation of 
~/.bashrc. Start from there a new emacs 
(by typing in 
emacs &
)

This will activate execution of ~/.emacs


Now open a file with extension .agda e.g. 
~/agda/myfirstagdaexample.agda

Then emacs will switch to Agda mode and you can start.


http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/index.html

contains the notes from the course

http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/agdalectureexamples/

contains the examples used in the lecture (there are only two
short examples)

If there are problems with the installation, please email me.

Enjoy,

Anton Setzer