Dear experts on antiquotations HOL4, I've looked through tools/Holmake/QuoteFilter, but could not read the input format -- I am used to functional parser combinators instead of lex + yacc.
Is there a specification of the input syntax in the documentation? But it is also changing occasionally, so it might be better to re-use the existing implementation. Ultimately I want to turn HOL4 ML source into tokens with precise source positions, e.g. byte addresses of the original string. The idea is to continue some experiments with HOL4 inside the Isabelle Prover IDE, see also https://sketis.net/2015/hol4-workshop-at-cade-25 Makarius ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
