Hello all,
What is the usual method for "viewing" a proof stored in HOL Light, if you
wanted to read it like a regular math textbook (assuming you can get over
syntax difficulties)? (Of course it is not really feasible to look at the
code in isolation, because you can't see the formulas.) The method I have
been using so far is to copy the tactics one at a time into a HOL session
using g() and e(), but it's very tedious and time-consuming, and it is also
difficult to undo if you make a copying mistake during the process. (I
should note that I am still a relative newbie to using HOL Light and this
is essentially the only thing I have tried to do with it - I have yet to
write an actual proof of my own in HOL Light.)
I feel like this is a common enough goal that there should be some program
to do what I am doing and log the output. Better yet, if there was a
website or downloadable collection of these proofs processed into a form
that did not require interactivity in the OCaml session, this would make it
much easier for mathematicians who do not necessarily want to write proofs
but want to examine the many existing HOL Light proofs in order to
understand them (like me). Does such a thing exist?
Mario Carneiro
------------------------------------------------------------------------------
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the
conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
