Notes on commands

• The assume command only exists in interactive proof mode, so we can't access it with eval. This causes the nub and qsort examples to fail. Another strange thing is that it only seems to work when its used in a file loaded by HERMIT from the command line. If I try to use it in the existing interactive hermit shell, it says the command isn't found.

• The following items fail in hermit-shell with the error "Rewrite failed:This rewrite can only succeed at quantified nodes.":

  • NewLast.hss works with hermit but not hermit-shell
  • new_reverse works with hermit but not hermit-shell

• In HERMIT, set-pp-width doesn't seem to do anything.

• In HERMIT, rule-to-lemma seems to only take one argument (the name of the rule) but the code indicates that it takes two (the first one being a PrettyPrinter). This first argument must be passed automatically at some point and we should figure out how to implement this in hermit-shell.

• What should be done about duplicates of commonly used Prelude functions like repeat?