2009-10-26から1日間の記事一覧
今日もTypes and Programming Languages (The MIT Press)に載っている定理の証明です。 type_dec 補題を定義する際に、以下のような定義が必要になりました。 Definition type_dec : forall t1 t2 : type, {t1 = t2} + {t1 <> t2}. で、これを証明するために…
30分プログラム、その683。シーザ暗号化をやってみました。 シーザ暗号がなんぞやかは、シーザー暗号 - Wikipediaを参考にしてください。 使い方 (* 3文字ずらす * - val (f,g) = make 3; val f = fn : string -> string val g = fn : string -> string (* …
