I am sure the technologies are fairly similar. In particular, the type of preterms exists in HOL-4 and all kinds of syntax manipulation can take place there before typechecking and term construction.
Konrad. On Thu, Oct 23, 2014 at 6:00 AM, Piotr Trojanek <[email protected]> wrote: > 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 >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
