You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, when you have some command, that outputs some info (like thm or term), this output is for a short moment, if at all, shown in the "Prover output" window. But this vanishes as soon as the prover advances.
So, an idea would be to have an additional window/view that holds those information. Perhaps in some way like "line number: message"
For example: 12: 'a list => 'a list 20: ?P => ?Q => ?P && ?Q
Advantage is: One is able to see the output at all. Additionally, one could see the output of multiple commands at the same time. For example in PG one can only see one output at the same time, so one has to toggle between to terms if one wants to compare them.
The text was updated successfully, but these errors were encountered:
Currently, when you have some command, that outputs some info (like
thm
orterm
), this output is for a short moment, if at all, shown in the "Prover output" window. But this vanishes as soon as the prover advances.So, an idea would be to have an additional window/view that holds those information. Perhaps in some way like "line number: message"
For example:
12: 'a list => 'a list
20: ?P => ?Q => ?P && ?Q
Advantage is: One is able to see the output at all. Additionally, one could see the output of multiple commands at the same time. For example in PG one can only see one output at the same time, so one has to toggle between to
term
s if one wants to compare them.The text was updated successfully, but these errors were encountered: