Agda入門会 in ie #1

イベント内容

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

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

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

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

注意事項

※ こちらのイベント情報は、外部サイトから取得した情報を掲載しています。
※ 掲載タイミングや更新頻度によっては、情報提供元ページの内容と差異が発生しますので予めご了承ください。
※ 最新情報の確認や参加申込手続き、イベントに関するお問い合わせ等は情報提供元ページにてお願いします。