Open mohrm opened 9 years ago
One use case is that you have a complete proof, and you select the parts of it you want to reuse for later. You don’t want them to disappear suddenly then :-)
What I’d rather like to see is that the selected blocks are then automatically replaced by the newly generated block. It might need a bit of additionally book-keeping to match the ports. I’m also worried about cases where the generated block is actually less powerful than the selected proof segment, so this feature should come after “undo” (#53) is implemented.
okay, replacing the proof with one block is also nice.
After I have exported a rule, the building blocks stay there. In most cases, I guess, I just need the rule and do not care about the proof, so how about making the proof disappear with a cool animation (e.g. blinking like in tetris)? ;) For cases in which the proof is still needed, one could just undo that.