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