3 ms·
It's very small so you can do it easily in clojure, https://github.com/the-little-prover/j-bob/blob/master/scheme/j-bob-lang.scm https://github.com/the-little-p
by kryptiskt 11y ago
It's very small so you can do it easily in clojure, https://github.com/the-little-prover/j-bob/blob/master/scheme/j-bob-lang.scm https://github.com/the-little-prover/j-bob/blob/master/schem... defines the language used and https://github.com/the-little-prover/j-bob/blob/master/scheme/j-bob.scm https://github.com/the-little-prover/j-bob/blob/master/schem... is the proof assistant. There's absolutely nothing fancy there.
- mcguire 11y ago"We include the necessary code to run J-Bob in ACL2 and Scheme, as well as a transcript of the proofs in the book. J-Bob is also included in the Dracula package for Racket." Isn't ACL2 Common Lisp based? If it runs on Scheme/Racket and CL (or at least ACL2), it should be pretty easy to translate. (ACL2? It's theorem provers all the way down!)