List of feature requests.
Each item is either ranked 1 (useful), 2 (really useful), 3 (important).
- (1) add dialog to RmLink
- (1) A proof is a tree. In a tree, a goal is associated with each node. Each node is annotated with a integer sequence (starting with the marker "top" which corresponds to the statement to prove) that depends on the node's location in the tree. For example, the first subgoal of the second subgoal of the proof of a lemma is annotated with the sequences "top 2 1". It could be useful instead to display, e.g., "top 2/3 1/2" if the top node had 3 subgoals and the second subgoal had itself 2 subgoals.
- (2) When interpreting EventML to Nuprl, it would be very useful to get at the end the list of the lemmas that haven't been automatically proved.
- (1) When searching for a pattern in a navigator, only clicking on the Reset* button will put the searched pattern in the list of previously searched pattern. It could be useful if once a pattern has been searched for, it is automatically put in that list.
- (2) Smart EventML to Nuprl re-interpretation.
- (1) We would like to be able to access nodes in a proof by just typing addresses such as "top 1 2 5 1 1".
- (1) Can we get the toploop to perform asynchronous computations?