https://twitter.com/kinaba のログ (twilog の方が便利です。)
| ぎゃあ間違っていきなり1000までやる方投げてしまった…！あなぷる鯖に猛烈に負荷をかけてしまっている気がするすみませんすみません | |
| @kikx すみません、とりあえず 1≦x≦50 の証明を投げてサーバでどのくらいの時間になるか見るつもりが間違えてx≦1000のまま投げてしまいました…orz | |
| 手元では4分くらいで終わる。ただ、各xに対してのCollatz xはCoqで作ってるんだけど1から1000までは結局Ltacでブン回しているだけなので本当はこちらもCoqで書きたいなーと思いつつ書けない | |
| @togashi_tv おお、情報ありがとうございます！そうですね、確かに早めにやっておいた方が良さそうです。 | |
| .@esumii さんの実況を見ている。Dagstuhl Seminar 一度行ってみたいなあ。行ってみたいというかつまり、呼ばれるような仕事をしろという話である。 | |
| Fibonacci function すっごいわざとらしく解いた。#anarchyproof | |
| テイルズは http://twitter.com/kikx/status/22434052724 を見て証明付コードの簡単な例を投げてみた。関数作らずxssの存在証明だけ書いて Extraction するとちゃんとtails関数が抽出されて面白いです #anarchyproof |