Dear all, is it possible to use HOL4 parser in a similar way to `parse_preterm` from HOL Light?
In HOL Light one can easily build a parser for HOL terms embedded in a custom language (see hol_light/Examples/prog.ml). In HOL4 it seems only possible to modify the term grammar (e.g. with add_rule), which is much less flexible. -- Piotr Trojanek ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
