Hi all,
I would like to add a pretty-printing rule to completely omit a constructor
and only print its argument. (I understand this means the resulting output
won't parse back to the same input without type inference help.) Is it
possible to do this in any way short of making a userprinter?
To
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
