これはTheorem Proving Advent Calendarの15日目の記事である。 二回目じゃないのかって？人数不足だ。気にしてはいけない。 さて、今日の記事が何に関する記事かは見れば一目瞭然。 Coqの中のtactics記述用言語Ltacについてであり、目標はあの有名なcrushを…

今b-mobileのSIMで使っていて、パケットを使いたくなかったのでDoCoMoショップに行ってみた。 聞いてみたところ、アップデートさせてくれるということで、SIMを持ってきてくれて、相手の目の前でアップデート。 無事できた。よかった。 と思ってたよ今日まで…

面倒な話である。 ソフト名はメモとるの忘れたため、詳細が全然わからない。 わかっている範囲： ans.exe*1という実行ファイルで、ユーザーのホーム\AppData\Localに実行ファイルを置いた。 32bitアプリケーションだった。 ブラウザが落とされた（侵入経路は…

先ほどの記事、12-03という日付になっているが、一応日付が変わってから公開している。 これははてなダイアリーの仕様*1なので、私に言われても困る。 *1:もちろん設定で変更可能、今はデフォルトの午前6時日付変更になっている。

これは、Theorem Proving Advent Calendarの四日目の記事である。 ぱっと見ではあまりTheorem Provingらしくないかと思われるかもしれないが、たまにはこういう話もよいだろう、ということで。 お題 今回使う道具は、Curry-Howard同型対応、直観主義で失われ…