Jacob Thomas Errington
Jacob Thomas Errington
I noticed cliff explosives are missing. If you could add them, that would be great!
This is related to #28 but more general. Resolving this would resolve #28, so that issue is invalidated by this one. We should also forbid duplicate theorem names, LF constructor...
* Subgoals are currently stored in a list, which does not reflect the tree-like structure of proofs. It would be great if subgoals were instead stored in a tree structure....
`total.ml` does not have an interface file despite defining tons of functions that are used only internally. In principle, these should not be exported, so one should add an interface...
It would be great if one could write `suffices by i` by itself and interactively fill in the concrete types of the arguments. That is, the interaction would look something...
My resolution for #68 is simply to change the error into a proper user error: right now there isn't much support for holes appearing in positions other than as terms....
I think the answer is yes. It should suffice to analyze the case-expression generated by the splitting to see if it is a unique case, and then to convert from...
The interactive mode presently communicates with emacs with an ad-hoc protocol. Instead, we should use an s-expression based scheme, which will facilitate deserialization on the Emacs end, and serialization on...
I try to write as much code documentation as I can. It would be great if we could integrate OCamldoc into the mix so that we can generate HTML documentation...
Load this signature. ``` kind : type. con : type. lam : kind -> (con -> con) -> con. app : con -> con -> con. cn-of : con ->...