関数型言語で reverse を書くときは let rec reverse1 = function | [] -> [] | x::xs -> reverse1 xs @ [x] ではなく let reverse2 = let rec aux xs = function | [] -> xs | y::ys -> aux (y::xs) ys in aux [] と書け，という話はまぁよく例として聞く気…

http://www.iij-ii.co.jp/lab/techdoc/coqt/ を読んでいたらいつのまにかそんなかんじのを書いていた．どうしても Vim で書きたいかわいそうな人以外は普通に CoqIDE や Proof General 使ったほうがいいと思います． https://github.com/eagletmt/coqtop-vim…

dynamic port forwarding ssh -D 1080 remotehost とか，~/.ssh/config に Host remotehost DynamicForward 1080 と書いて ssh remotehost すると，1080番ポートで SOCKS プロキシサーバを立てられる． firefox のような SOCKS プロキシに対応したソフトウェ…