lcdoutlet/hol-light repository overview

Testing hol-light theorem prover https://github.com/jrh13/hol-light⁠

http://www.cl.cam.ac.uk/~jrh13/hol-light/⁠ http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf⁠ https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf⁠

cd hol-light

run ocaml -I `camlp5 -where` camlp5o.cma

then run #use "hol.ml";;

you should expect to see several theorems proved and a series of tests run. It should take 1-2 min.

for a better repl opam install utop utop -I `camlp5 -where` camlp5o.cma

For some reason back ticks yield a syntax error in utop.