I did look at monadsyntax.sml at the very beginning. I should have
revisit this file when I started to implement my postprocessor...
I decided to keep the global grammar free from any extensions
(especially while experimenting), so I did not use
add_absyn_postprocessor. I call my parser with
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),
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
