iPodでclojureのソースコードを読みたかったのです。 find . | awk '/.clj$/ { print "echo",$0; print "cat -n ",$0 } ' > list.shlist.shを実行してできたテキストファイルをPDFに変換すれば、通勤時間でも手軽にコードリーディングできる。

http://kurohuku.blogspot.com/2011/05/nil.htmlCommon Lispではdeftypeで型を定義するときに、 任意の条件が記述できるということか。 Clojureでもできないか、やってみよう。

型定義とパターンマッチが使えるライブラリ。 MLっぽいことができる。 (ns calc (:refer-clojure :exclude (deftype)) (:use [clojure.contrib.types :only (deftype defadt match)])) (defadt ::weekday Sunday Monday Tuesday Wednesday Thursday Friday S…

http://lisperati.com/vijual/ ASCIIアートでグラフを描くライブラリ。

https://gist.github.com/986500書きかけですが。 あとは、全部のノードパターンを網羅するようにして、 同型性判定できればよいはず。 こちらはCommon Lispのグラフ操作ライブラリ。 https://github.com/masonium/cl-graph エルデシュの論文収集プロジェク…

https://gist.github.com/986288参考サイト： http://www.kashi.info.waseda.ac.jp/~kashi/lec2000/jsj/queen/ ここのサイトでは、「問題をいきなり解くのは難しいので・・・」 と書いてあるので、あえて問題をいきなり解いてみた。

Chapter 2の演習が一通りできたのは良かった。 参加者の皆様に感謝。http://www.slideshare.net/kencoba/awodeytokyo-20110521 iPod touchだと画像が荒い。次回は6/18 13:00-19:00 新宿三井ビル 34Fの予定。

バッハの無伴奏バイオリンパルティータから、SarabandeとDoubleを演奏。 次回の課題は 右手運指を完成させること。 脱力ではなくリラックスすること。 本番の日は音量を本番と同じにして弾くこと。 視聴者と一緒に曲を楽しむこと。

Prelude なにげにClojureのお話 Awodey 2.8 Exercises 2.8.1 背理法を使わないで証明する方法はないか。 コンセプタンでoto_oto_otoさんが、背理法以外の証明法を紹介していました。 http://d.hatena.ne.jp/oto-oto-oto/20110406/1302109498 http://d.hatena…

(pmap #(do (Thread/sleep (* %1 1000)) (println %1)) '(5 1 3 6 2)) これだけ、なんだけどいまいちうまく表示してくれないなぁ。と思ったら@omasanoriさんから。 (dorun (pmap #(do (Thread/sleep (* % 1000)) (println %)) [5 1 3 6 2])) dorunなのね。あ…

ClojureのParser Combinator。 これは真面目に調査しよう。https://github.com/joshua-choi/fnparseサンプル http://slyrus.github.com/2010/09/17/parsing-smiles-with-fnparse.html

http://www.jitec.jp/1_13download/hani20061107.pdf を仕様として作成中。https://gist.github.com/980285普通に2パスでラベル解決->コード生成。 いくらなんでも書き捨てレベルなので、リファクタリングせねば。「名前付けはそのプログラミング言語の文化…

ちょこちょこと設定手順が変更されているClojure on Emacs. 手順をまとめる。 project.cljに以下を追加 :dev-dependencies [[swank-clojure/swank-clojure "1.2.1"]] コマンドラインから、 > lein swank Emacsにて、 M-x slime-connect 127.0.0.1 4005なんだ…

AwodeyのP33にProjective Objectのお話が載っているのですが。Alloyで書くとこういうことなのかな。 https://gist.github.com/967745たけをさんから以下のような例をいただいた。 open util/relation sig P { f : one X } sig E { e : one X } sig X {} fun …

http://blog.starbug1.com/archives/584いろいろと参考になる要素がつまっているのでメモ。

P18に掲載されているものをCoqで。 http://gist.github.com/963772 Pab Pba ----------------------------- split. forall x, exists y,Pxy Pab & Pba ---------------------- -------------------- exists y. exists y,Pay. exists y,(Pay & Pya). --------…

http://d.hatena.ne.jp/sirocco634/20090523/1243049860 こんなのを見つけたのです。Clojureでやってみた。 https://gist.github.com/962101 カード番号は文字列として渡してあげます。

https://sites.google.com/site/clojurejapanesedocumentation/Clojureの日本語ドキュメントを整備しようというプロジェクトがあるようだ。 私も協力しようかな。

Prelude TAPL読んでることだし、FM_Forumでも型付きラムダ計算やってみるか Isabelle/HOLもやってみたい TAPL読書会は第２週で固定しましょうか http://staff.aist.go.jp/reynald.affeldt/seplog/ cocoatomoさんのTAPL発表資料 https://github.com/cocoatomo…

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011/doc/tutorial.pdfhttp://gist.github.com/958500うーむ、ぜんぜんわかってない。特殊記号の入力で手惑う。 Isabelles2011/etc/symbolsにProofGeneralが補完している特殊記号のテーブルがあ…

http://partake.in/events/dfc10138-1c40-449a-84eb-121944653e58というわけで、次回は6/4 13:00-19:00を予定しています。 Coq使いはだいぶ増えましたが、他のツール使いはどうだろう。

とりあえずメインのページつくった。 http://partake.in/events/ac41261d-6026-4d09-8814-5ad3e58446e8懇親会はこちら。 http://partake.in/events/cb7c0530-0c46-4dd5-a945-032a2af46e1b懇親会は立食パーティ形式にして、LTでもやりましょうか。

http://save.sys.t.u-tokyo.ac.jp/~yusa/fonts/ricty.htmlプログラミング用フォント

証明途中ですが。https://gist.github.com/954854

議題 名前空間を完全に分離したいときは、ファイルを分けるのが無難。 Coq内でのLoad Pathの設定方法 Add LoadPath "~/src/coq/ConCaT" as ConCaT. Print LoadPath. Require Export ConCaT.SETOID.Map2. structureをlocalにできるのか？ ConCaTのインストー…