Vince, thanks for fixing my error! This works now:
let parse_qproof s = (fst o parse_preterm o lex o explode) (String.sub s 1
(String.length s - 1));;
Now I get the same output for both
`;&1 + 1`;;
and, with your new quotexpander,
`'&1 + 1`;;
val it : preterm =
Combp
(Combp (Varp ("+", Ptycon ("", [])),
Combp (Varp ("&", Ptycon ("", [])), Varp ("1", Ptycon ("", [])))),
Varp ("1", Ptycon ("", [])))
That's great you're changing your Q-like module right now to use the parser
instead of strings. Let me be more precise about environments, or as precise
as I can be with my poor understanding of how words like scope and variable
binding are used in HOL. Let's say in HOL Light that a free variable
occurrence is in the scope of a variable binding. I think the variable is
given the bound value, if we type it correctly, but its type is not inferred.
I think the type ought to be inferred, and that's what Freek does in miz3.ml,
by changing the parser, partly with his parse_qproof line in quotexpander.
--
Best,
Bill
------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
