...
- (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 interpreting EventML -> to Nuprl is done , it would be very useful to get a 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?