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

Reply via email to