Coq などの定理証明系に興味を持っている人は少なくないと思うのですが、やっぱり最初の一歩を踏み出すのは大変。web 上の Coq チュートリアルは、Coq 処理系の機能を説明しているだけで、数学の素養がない人(普通の情報系の学生)が実際に関数の性質を証明す…

一覧表示 スライドショー中 ちょっと前に最近の CSS のおもしろさを知ったので、プレゼンテーションを作れるライブラリ的なものを作ってみた。ページの切り替えや一覧表示のときにぬるっと動きます。id:amachang さんの作った s6 と比べると、(CSS さえ書け…

寝る前に OCaml でなんか書いてみるか、と思って書いてみた。 exception Unexpected_char let interpret str = (* バッファ *) let buf = Array.create 3000 0 in (* 対応する右括弧(])を探しに行く *) let rec rp idx n = match String.get str idx with | …