https://twitter.com/kinaba のログ (twilog の方が便利です。)
| 僕が整数関係でCoqで書く証明は apply (結合|交換|分配則,推移律)/rewrite/change/replace のものすごい連打になってしまうので、もっと綺麗に書く方法をちゃんと身につけるべきだなあ… | |
| @heppoko_maid 一撃でゴールが示せるケースよりも、帰納法の仮定やLemmaを使うために部分式をいい形に書き換えたい、という機会が多くて、replace (たいへん長い式) with (たいへん長い式) by omega. とかの連発になってしまうのですよーどうも。 | |
| @d_kami @rofi とりあえず修正done。ありがとーございます | |
| ブログの感想で「わかりやすすぎて当たり前に見えちゃう」と思って頂けるのは基本的にとても嬉しいのですが、一昨日書いた階乗の話は、いざ書くと自分でも当たり前に見えすぎて一体何を凄いと思ったのかすらわからなくなってしまい、俺はいったい何に感動してたんだ？？？と思いながらうｐしたのですが | |
| 自分でもよくわからなくなってるそれが伝わった http://twitter.com/Constellation/statuses/23068189180 http://twitter.com/mr_konn/status/23129087166 http://twitter.com/sumim/status/23135199835 みたいでよかった。@herumi さんの下さった更なる例が面白い→ http://homepage1.nifty.com/herumi/diary/1009.html#6 | |
| @mr_konn 決定不能の会 http://pira.jp/undecidable/ で聞いたのですが、毎回怪しげなの（例： 一般化コラッツ予想の回 http://twilog.org/xagawa/hashtags-fractran）が登場して面白いのでいらっしゃるとよいです。問題は次回の予定が決定不能なことですが… | |
| QuineやPolyglotの仲間で、エッシャーの http://www.google.co.jp/images?q=%E3%82%A8%E3%83%83%E3%82%B7%E3%83%A3%E3%83%BC+%E9%B3%A5+%E9%AD%9A 的コードって書けんかな、と考えてる。#ocamlmeeting のTシャツ見せてもらったのがラクダ＆ラクダタイリングだったので連想。上部はPerlラクダで段々OCamlに変わってくとかで | |
| 般若心経ポップ http://www.nicovideo.jp/watch/sm11982230 いいなあ。歌詞コメ良い。すごい良い。読んだことなかった。こう盛り上がりをじわじわ増してピークで抜ける構成の歌詞、歌詞じゃないや、なんだ念仏なんだなあ。見事な構成だ。お経凄い。 | |
| @zakkas783 カンダタこぶんでございます。@finalfusion さんがカンダタのリクエストがあったので微妙にひねってみた。 | |
| @tri_iro 停止問題と同じTuring degreeの決定不能問題ばっかりだと飽きるなー、というのがあって、それより下の話も（ちゃんと見るにしろ深追いはしないで引き返すと決めるにしろ、その判断できる程度には）一応は知っておきたい気分があります＞優先度法。応用は…編み出す！ |