Open roboguy13 opened 9 years ago
We should be able to modify scripts to now use getPP
in order to call ruleToLemma
directly.
However, my initial testing is showing that these functions still fail, but I believe it's due to the DocH
return value and not because of the PrettyPrinter
arguments.
Commit https://github.com/ku-fpg/hermit-shell/commit/773e016783fcd5105e8fd4f089926d9fddee50c0 should have us ready for this.
As a heads up, we'll probably have to regenerate the golden output for some tests since we may change the output of scripts when moving away from eval
.
Currently, the only calls to
eval
are to userule-to-lemma
.eval
is used here due to the pretty printer.