Le 02.04.13 22:33, Bill Richter a écrit : > Vince, this is great! May I ask you to learn about miz3? Well, it's on my TODO list, but not in the short term... > With a little work, I think miz3.ml can be turned into a general purpose > interface for HOL Light, with much improved readability, with fewer type > annotations in particular. I work on this too (see, e.g., the module I refered too previously, or the tactics that I regularly present on this mailing list), but I generally prefer the usual tactic style rather than the declarative style. > Then each time you type something that starts with a semi-colon > (e.g., `;blabla`), you obtain the intermediate preterm instead of > the term. If I'm right, this means that you don't have the > backslash problem anymore (since we're going through the John's > parser), but not all the types are infered since we didn't go > through the type checking phasis yet. And you could define a > function disj_preterm easily (once you built your preterm, it is > easy to get the term by using term_of_preterm, generally composed > with retypecheck in order to check that the final term is well > typed). > > Thanks! You're explaining something about miz3 I never understood. (...) > The function thm is applied to a term that begins with a semicolon! > Just as you said! Wait, this is absolutely random: I don't know anything about miz3, so I don't know what the semicolon represents w.r.t miz3 internals. I just happened to use a semicolon because I needed a way to distinguish from usual quotations and it was close to a colon (used for type quotations), but it has nothing to do (a priori) with miz3 semicolon.
> And maybe as Freek said, we'd be better to use a different character, and I > see where you use the semicolon, in the if String.sub s 0 1 = ";": Exactly. > OK, I'll go play with that! I hate to be picky, but > > 1) Freek does not use quotexpander in miz3.ml Again, I don't know anything about miz3 (and don't have any time to spend on it right now) so maybe he's using a trick that I didn't think of. > 2) Is there any way to get rid of the initial semicolon? Well you just need a way to make a distinction with usual term quotations (`bla`) and type quotations (`:bla`). You can either find another prefix character (e.g., `'bla`) or a suffix one (e.g., `bla.`) (I find the ending dot cool too), or any exotic way if you like (e.g., a '$' sign in the 4th position, or a # sign at every prime number position, well whatever you like...). Cheers, -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ ------------------------------------------------------------------------------ Minimize network downtime and maximize team effectiveness. Reduce network management and security costs.Learn how to hire the most talented Cisco Certified professionals. Visit the Employer Resources Portal http://www.cisco.com/web/learning/employer_resources/index.html _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
