Can someone explain the point of HOL Light parsers, as in the reference manual
entry for many:
This is one of a suite of combinators for manipulating
``parsers''. A parser is simply a function whose OCaml type is some
instance of :('a)list -> 'b * ('a)list. The function should take a
list of objects of type :'a (e.g. characters or tokens), parse as
much of it as possible from left to right, and return a pair
consisting of the object derived from parsing (e.g. a term or a
special syntax tree) and the list of elements that were not
processed.
I can see the parser suite is used heavily in parser.ml, and also Freek's
miz3.ml. I don't know if I need the parser suite, as my string/regexp miz3
tactics-proof interface is coming along fine, but I am curious.
Here's another question, unfortunately stated without an example. Suppose we
have a goal g which we want to prove with
MESON_TAC[th1; th2; th3];;
What's the difference between this and instead using MP_TAC to make the goal
th3 ==> g
and trying to prove this with
MESON_TAC[th1; th2];;
I have evidence that sometimes the 1st works when the 2nd does not. I don't
have an example when the 2nd works and the 1st does not. Why are the two
approaches not identical?
--
Best,
Bill
------------------------------------------------------------------------------
Try New Relic Now & We'll Send You this Cool Shirt
New Relic is the only SaaS-based application performance monitoring service
that delivers powerful full stack analytics. Optimize and monitor your
browser, app, & servers with just a few lines of code. Try New Relic
and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_may
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
