■

どうでもいい日記でも一日空くと大分やる気が落ちるね。

カナ漢字変換に、uim-skkを使ってるんだけど、かなモードで記号が全角になるのが気になるんでどやってカスタマイズするのか調べてたら、uim自体ほとんどschemeで書かれてんのね。
カスタマイズは ~/.uim というファイルに以下のような感じで

(require-module "skk")
(define skk-ja-rk-rule
  (append '(
    ((("z" " "). ())("　" "　" "　")) ;; z spaceで全角スペース入力
;; ここに追加すべし
    )
  skk-ja-rk-rule))

書いていけばいいらしい。まだやってないけど。
https://code.google.com/p/uim-doc-ja/wiki/CustomizeUim#uim-skk

Coqはどんどこ難しくなるな・・・

Inductive R : nat → nat → nat → Prop :=
   | c1 : R 0 0 0
   | c2 : ∀ m n o, R m n o → R (S m) n (S o)
   | c3 : ∀ m n o, R m n o → R m (S n) (S o)
   | c4 : ∀ m n o, R (S m) (S n) (S (S o)) → R m n o
   | c5 : ∀ m n o, R m n o → R n m o.

にて

練習問題: ★★★, optional (R_fact)
関係 R の、等値性に関する特性をあげ、それを証明しなさい。 それは、 もし R m n o が true なら m についてどんなことが言えるでしょうか？

どんなことが言えるの？
o はev o くらいは言えそうだけど。c4が無ければ double(m + n) = o くらいは言えるかな？