Mostly Agda code for a course and blog on "Logic, Types and Spaces"
###Getting Agda:
####For Ubuntu 64-Bit:
- Open your terminal and run the following commands
sudo apt-get install emacs libgmp-dev zlib1g-dev libncurses5-dev
wget http://bit.ly/1xKVN5u #This file will take a little while to download (195MB).
cd \
sudo tar xvf ~/haskell-platform-2014.2.0.0-unknown-linux-x86_64.tar.gz
sudo /usr/local/haskell/ghc-7.8.3-x86-64/bin/activate-hs
cabal update
cabal install alex
cabal install happy
cabal install cpphs
sudo cabal install --global Agda
agda-mode setup
agda-mode compileA short Tutorial for Agda development in Emacs
####Some Agda commands in Emacs
| Keybinding | Description |
|---|---|
| ctrl-c ctrl-l | Load File |
| ctrl-c ctrl-x ctrl-c | Compile File |
| ctrl-c ctrl-x ctrl-q | Quit Agda mode |
| ctrl-c ctrl-x ctrl-r | Kill and Restart Agda |
| ctrl-c ctrl-c | Case split |
| ctrl-c ctrl-r | Refine goal |
| ctrl-c ctrl-f | Next goal |
| ctrl-c ctrl-b | Previous goal |
| ctrl-c ctrl-n | Evaluate an expression |
| ctrl-c ctrl-d | Infer (Deduce) type |