Le 16.04.13 00:30, Bill Richter a écrit : > Thanks, Vince! It worked, once I substituted your quotexpander into > system.ml and restarted HOL Light with > ocaml > #use "hol.ml";; > > Now I can get to work on your exercise. A few questions: > > Why didn't my attempt work? Why did I get the error message "Exception: > Noparse." from > > let parse_qproof string = (fst o parse_preterm o lex o explode) string;; > `;&1 + 1`;; > > It doesn't look that different from your fix: > > else if c = ";" then "parse_qproof \""^(String.escaped s)^"\"" > else if c = "'" then "(fst o parse_preterm o lex o explode) \"" The answer actually comes from the next line, I let you check. The problem was that the string was passed to parse_qproof without removing the ";".
> > since others might benefit from having quotations dedicated to > preterms (as it is the case for instance in HOL4). > > That's very interesting. Can you say more? For instance, my Q-like module would benefit from using this instead of strings as it is doing right now. > And what do you think of Petros's interesting IsabelleLight possibilities? No idea, unfortunately I have only a shalow knowledge of it... > Would it be possible, do you think, to maintain an environment which would > get rid of repeated type annotation without changing the parser? Could you be more precise? -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ ------------------------------------------------------------------------------ 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
