イベント内容

Agda入門会 in ie

Agda の入門会です．
今回は，自然数を定義するところから始まり，加法，減法，乗法などを定義します．
その後，可換則（交換律）などが成り立つことを証明していきます．

事前準備

Agda を実行できるようにして下さい． Emacs の agda-mode を使うと幸せになれます．

brew が入っている場合，以下の手順で準備終わると思います（emacs も新しい物が入っている方が良いです）．

brew install agda --HEAD

インストール完了時に表示される以下のコマンドを実行します．

mkdir -p ~/.agda
echo /usr/local/lib/agda/standard-library.agda-lib >>~/.agda/libraries
echo standard-library >>~/.agda/defaults

その後

agda-mode setup

とかすれば環境できると思います．

※ 環境が作れなくても当日フォローします

場所はおさえ次第更新します

注意事項