List of feature requests.
Each item is either ranked 1 (not important), 2 (really useful), 3 (important).
- (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 the interpretation EventML -> Nuprl is done it would be very useful to get a 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 -> Nuprl re-interpretation.