Hi Bill, Le 01.04.13 22:08, Bill Richter a écrit : > 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? Yes. > 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? I'm not sure I see what you mean here, could you be more precise?
-- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ ------------------------------------------------------------------------------ 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
