出た。 http://userweb.cs.utexas.edu/users/moore/acl2/Alloyが一段落したら挑戦します。

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"…