Thanks, Vincent and Petros! I'll have to study your interesting posts carefully. A few quick comments:
Petros, it looks like you're doing something that's a whole lot more interesting than my project. I'm not sure I have the terminology straight: Suppose we bind a variable x, say with INTRO_TAC, DESTRUCT_TAC or X_CHOOSE_THEN, to a term t with type alpha. Then if the variable x occurs in a term (in doublequotes) that is in the scope of this variable binding, x ought to automatically be bound to t:alpha. We should not have to repeat the type annotation of x. If that's what you did, Petros, that's fabulous, and will cut down on more type annotations than my consider/case would. Freek's miz3 does something like this I think, and I haven't figured out how he does it. Can you comment on your Isabelle Light code? I'll go read your paper with Jacques Fleuriot link.springer.com/chapter/10.1007%2F978-3-642-16242-8_40 The other alternative, which is the one you required in your previous email, is to make use of the built-in term parser in order to avoid the parsing problems of the first alternative, then go back to strings by using a function that you called "TermToString", which exists in HOL Light, except that it's called "string_of_term". Thanks, Vincent, and I think I have to go this way, but string_of_term doesn't do what I want, because it loses my explicit type annotations. How can I go about learning how to use the built-in term parser, and which parser do you mean? I believe that pa_j.ml defines how backquotes work in HOL Light, and that pa_j.ml gets compiled by make. Is that right? Just to be a bit more precise, the ocaml function ^ that concatenates strings obviously has to know what strings look like internally. Even beginners know how to write a recursive function that concatenates two lists, but of course you have to know about cons (::), car (sometimes hd), & cdr (sometimes tl) to do it. Some similar knowlege is needed to write ^, and probably even more knowledge is needed to join two terms with an \/, but I don't see why it can't be done, given sufficient knowledge of camlp and pa_j.ml. Now is that right? -- Best, Bill ------------------------------------------------------------------------------ Own the Future-Intel(R) 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://altfarm.mediaplex.com/ad/ck/12124-176961-30367-2 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
