~malo/KripkeLabb.agda
Detta är en relativt svår labb och kommer alltså att ge 2 bonuspoäng för VG. För att komma igång med Agda så finns en liten övningsfil med några enkla uppgifter i satslogik (och en i predikatlogik):
~malo/uppvarming.agda
För att starta Agda (vilket sker när man öppnar en fil som slutar med .agda i emacs) så måste du skapa filen .emacs och däri lägga raderna
(defconst agda-startProg "/users/mdstud/malo/Agda/emacsagda" -H40Mg) (autoload 'agda-mode "/users/mdstud/malo/Agda/agda-mode.el" "Major mode for Agda files" t) (setq auto-mode-alist (cons '("\\.agda" . agda-mode) auto-mode-alist)) (remove-hook 'hugs-mode-hook 'turn-on-font-lock)
eller kopiera filen ~malo/.emacsagda till .emacs hos er.
På Agdas hemsida finns mer information om Agda.
Thomas Hallgren har jobbat med Alfa så att det går att göra
Kripkelabben i även Alfa. Ni måste då göra
setenv ALFA Alfa-new
innan ni startar Alfa, annars får ni den gamla versionen Alfa (som vi låter ligga kvar för säkerhets skull).
~malo/KripkeLabb.agda innehåller en del kommentarer inne i deklarationer, så får man inte ha det i Alfa; dessa är borttagna i
~malo/KripkeLabbAlfa
som alltså är den ni skall ladda in i Alfa. Obs! i det här beviset skall man inte använda ND style proof!