CommonLispにもML系Matchがないのか。 (in-package "ACL2") (defun not-3 (x) (cond ((equal x "yes") "no") ((equal x "no") "yes") ((equal x "maybe") "maybe"))) (defun and-3 (x y) (cond ((and (equal x "yes") (equal y "yes")) "yes") ((and (equal …

某ProofCafeではCoqでやってみたという話の、 リストの反転問題。 reverse (reverse xs) = xs http://study-func-prog.blogspot.com/2010/04/coq-reverse-reverse-xs-xs.htmlACL2ではどうなんのかな、と思ってやってみた。 環境はACL2s。 (in-package "ACL2"…

clojure.contrib.typesの使い方がいまいち分からない。 もうちょっと賢いマッチングしてくれないのかな。 (use '[clojure.contrib.types]) (defn not-3 [x] (match [x] [:yes] :no [:no] :yes [:maybe] :maybe)) (defn and-3 [x y] (match [x y] [:yes :yes]…