最近Coqが流行してるので、ボクも流れに乗ってみました。今回、ボクが証明したかったのは、2回reverseすると元に戻るという性質です。 Theorem RevReflect : forall {A : Type} {xs : list A}, reverse (reverse xs) = xs. そののために、appendを定義したり…

30分プログラム、その664。ErlangでファイルのMD5計算をやってみました。 本当は、md5ベースで重複ファイルの削除をするぜ、みたいなことをやりたかったんです。でも、特定ファイルのmd5を計算するだけで時間が立ってしまいました。特にio_lib:formatに渡す…