Agda を使ってみる

Proof Summit に参加している。

Agda を初めて使う。
インストールは 掲示板で紹介されていた ここ を参照した。

Ubuntu 8.04 LTS では…
sudo apt-get install agda-mode
sudo apt-get install agda-stdlib
で使えるようになった。

yoshihiro503 さんのサイトを参考に実行した。
./src/myFirstAgda に hello.agda を用意。

module hello where

open import IO
main = run (putStrLn "Hello, あぐだ World!")

ここで、C-c C-l で型チェック、C-c C-x C-c でコンパイル。
./hello ができるので、実行できる。
文字コードは、UTF-8 だ。

文字コードが UTF-8 のため、数学の記号がそのまま使えるようになっている。
打ちにくい…。

Agda の情報は、Agda Wiki が総本山のようだ。

# Mac のカスペルスキーが暴走する話を書こうと思ったが、いろいろあって消した。
# 暴走するよね、あれ。