Coq

reverse

Coq

関数型言語で 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 [] と書け,という話はまぁよく例として聞く気…

coqtop を Vim の中で動かして連携させる

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