Thanks, Ramana! You're the person I wanted to talk to. I already had a vague understand of what you explained (thanks for explaning), but I have a different question about HOL4:
I'm convinced that the solution to my problem involves camlp (I use camlp5-6.05), as I can't find anything in the HOL Light or Ocaml dox. So I think this is a parsing issue, and I'd like to understand what HOL4 that's analogous to the HOL Light camlp5 parsing that allows us to put terms in backquotes (or back-ticks as the HOL4 dox say). So can you describe the what HOL4 does that's comparable to the HOL Light use of camlp? I bet it will be easier for me to understand. For starters, why does HOL4 use double backquotes instead of HOL Light's single backquotes? The real piece you need, however, is the fact that Term does type-inference. I'm not sure if there is anything in HOL-Light already that does type-inference (as opposed to type-checking). That's encouraging for my project! I bet you're right. I bet preterm_of_term doesn't do type-inference and it's the later function term_of_preterm that does type-inference. Certainly the first place in preterm.ml where the string "infer" occurs is as an error message in term_of_preterm. Let me clarify what I want. Take two blocks of text t1 and t2. I want a functions like disj_term so that evaluating disj_term `t1` `t2`;; yields `t1 \/ t2`. That's not going to be possible if HOL Light does type inference on `t1` and `t2 before disj_term goes to work. And I'm sure from Freek's miz3 that HOL Light does not perform such type inference. -- Best, Bill ------------------------------------------------------------------------------ Own the Future-Intel® Level Up Game Demo Contest 2013 Rise to greatness in Intel's independent game demo contest. Compete for recognition, cash, and the chance to get your game on Steam. $5K grand prize plus 10 genre and skill prizes. Submit your demo by 6/6/13. http://p.sf.net/sfu/intel_levelupd2d _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
