clj-bob:Clojure的The Little Prover的J-Bob证明助手

clj-bob Daniel P. Friedman和Carl Eastlund的的证明助手的Clojure（技术上）端口。 注意事项 好的，所以首先，这不是正常的Clojure。 像Scheme实现一样，这主要是基于ACL2语法运行/仿真的宏和函数。 一方面，这真的很奇怪。 另一方面，这意味着在几乎所有情况下这都与这本书完全匹配-这是值得的交易。 我已经成功测试了本书的许多示例（包括最后一个示例），并且它们都与Scheme实现相匹配，但是就保证而言，这是我现在能给您的最好的示例。 奇怪的东西 这本书/ J-Bob认为. 和/在函数名称中合法使用。 不幸的是，克洛瑞尔不同意。 通过使用先进的search-and-replace:trade_mark:技术，我改变了所有. s和/ s变成- 。 这意味着， chapter1.example1现在是chapter1-example1 ， dethm.set?/