Learn You An Agda - TOC
1. Introduction 1.1 About this tutorial Step One: Learn Haskell 1.2 What is Agda, anyway? Types are Propositions 1.3 How do I get started? 2. Hello, Peano 2.1 Definitions, Definitions Hold on a second, types have types? Structural Induction 2.2 One, Two… Five! 2.3 Our First Check “I have merely proven it correct” 3. Propositions and Predicates 3.1 “Logic is the art of going wrong with confidence”
ブラウザ上でAgdaを試せるサイトを作ってみた - ぼくのぬまち 出張版
この記事は Theorem Prover Advent Calendar 2014 の4日目の記事です． Agdaがコンパイルできないんだがとか，agda-modeってEmacsだけなんでしょ？とか，そういった話をちょくちょく耳にするし，ProofSummit2014で明日の記事担当のamutakeくんがブラウザからCoq使えるやつを発表してたりしたので，Try Agda というサイトを作ってみた． リポジトリはここ https://github.com/notogawa/agda-interactive-server バックエンドはHaskellでwai+warp+websocketでAgdaのライブラリからAgdaを直に利用．フロントはjquery+ACE editor．画面レイアウトはもちろんbiim兄貴リスペクトだ． サーバ強くないし，あんまりデカい証明に使ったりするとガバガバなリ
Agda の入門の要約
Menu Menu top : Agda による圏論入門 ここで使われている例題は、 Category exercise in Agda に置いてあります。 Agda の install の方法 Homebrew を使うのが良いそうです。 Emacs を先に入れます。 brew tap caskroom/cask brew cask install emacs その後、 brew install agda GHCが入ってないなら、 brew install ghc install 先がどこかは、 /usr/local/Cellar/agda/2.5.2/lib/agda などになるので、~/.emacs.d/init.el に以下のファイルを置きます。あるいは自分のinit.el に適当に追加します。 init.el GUI 側で使わないと文字化けすることがあるようです。 Terminal
はてなブログ | 無料ブログを作成しよう
聖蹟桜ヶ丘へ 今年度の授業が全て終了した。最後の授業はテスト返却とその確認作業の後は特に何をしろとも言われていなかったので、『耳をすませば』の後半、お姉さんと雫が言い争いをする場面を生徒と皆で見た。 この場面。あの場面、お姉さんは雫に「今しなきゃいけないことから逃…
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
https://www.cs.gunma-u.ac.jp/~hamana/Papers/ppltut.pdf
