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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
