Michael Norrish
Michael Norrish
Some work in this direction appeared in 91d667670e8
I'd be happy to see this code integrated if you think it's useful. (You've tried using it.)
The important current use-cases: - `hol repl` starts the repl for interactive proof - `hol lsp` starts an LSP server - `hol buildheap` builds a heap - `hol runscript` runs...
Two fewer characters and it's just a single token, duh. :-) But yes, if you just scan all the arguments and don't find a sub-command, assuming `repl` to be the...
I view this as a feature request to improve/adjust the metis-encoder.
Seems like your storage of additional case-Eq theorems, and the functions for adding them, should be using ThmSetData.
Actually, the branch is `cons-append-norm` (hyphens, not underscores).
As per work done in ad11e1b42fe716e, it's not so clear to me that we need to right-associate. Instead, we can just add one extra rewrite ``` (xs ++ (h::t)) ++...
Good ideas!