Should have mentioned that you should have a look at
src/parse/Preterm.{sig,sml}
to start.
Konrad.
On Thu, Oct 23, 2014 at 4:59 PM, Konrad Slind <konrad.sl...@gmail.com>
wrote:
> 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 <piotr.troja...@gmail.com>
> 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
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
>
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
