お知らせ 【メンテナンスのお知らせ】4月25日(木)10:00から1時間半ほど、メンテナンス作業を予定しております。作業の間はconnpassのご利用が出来ません。ご迷惑をおかけしますが何卒ご了承ください。

お知らせ connpassではさらなる価値のあるデータを提供するため、2024年5月23日(木)を以ちましてイベントサーチAPIの無料での提供の廃止を決定いたしました。
2024年5月23日(木)以降より開始予定の「connpass 有料API」の料金プランにつきましてはこちらをご覧ください。
なお有料の対象となるのはAPIのみであり、connpassのサービスにつきましては今後も無料でご利用いただけます。

このエントリーをはてなブックマークに追加

4月

29

 Agda入門会 in ie #1

自然数を定義して遊び倒す会

募集内容

参加枠1

無料

先着順
6/10人

申込者
zeronosu77108
りゃま
わっしょい
ponyonyon
kanekou
たーりょう
申込者一覧を見る
開催日時
2019/04/29(月) 13:00 ～ 18:00
Googleカレンダー icsファイル
募集期間

2019/04/13(土) 13:13 〜
2019/04/25(木) 18:00まで

会場

琉球大学工学部

沖縄県中頭郡西原町千原(工学部)

マップで見る

イベントの説明

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

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

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

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

発表者

zeronosu77108 zeronosu77108

資料 資料をもっと見る／編集する

フィード

zeronosu77108

zeronosu77108さんが資料をアップしました。

2019/04/29 19:06

zeronosu77108

zeronosu77108 さんが Agda入門会 in ie #1 を公開しました。

2019/04/13 13:13

Agda入門会 in ie #1 を公開しました！

zeronosu77108

zeronosu77108 さんが Agda入門会 in ie #1 を公開しました。

2019/04/13 13:12

Agda入門会 in ie #1 を公開しました！

グループ

ie-functional

イベント数 7回

メンバー数 17人

終了

2019/04/29(月)

13:00 〜 18:00
Googleカレンダー icsファイル

開催日時が重複しているイベントに申し込んでいる場合、このイベントには申し込むことができません

募集期間
2019/04/13(土) 13:13 〜
2019/04/25(木) 18:00

イベントへのお問い合わせ

会場

琉球大学工学部

沖縄県中頭郡西原町千原(工学部)

管理者

参加者（6人）

zeronosu77108

zeronosu77108

Agda入門会 in ie #1 に参加を申し込みました！

りゃま

りゃま

Agda入門会 in ie #1に参加を申し込みました！

わっしょい

わっしょい

Agda入門会 in ie #1に参加を申し込みました！

ponyonyon

ponyonyon

Agda入門会 in ie #1に参加を申し込みました！

kanekou

kanekou

I joined Agda入門会 in ie #1!

たーりょう

たーりょう

Agda入門会 in ie #1 に参加を申し込みました！

参加者一覧（6人）

キャンセルした人（2人）