vscoq
vscoq copied to clipboard
Published
20 hours ago •
coq-community
coq-community
Feedback to empty Search
As Search goes to the output window it would be nice that there will be delimitators (specially when the result is void)
Search nat bool.
could output
"Search nat bool" gives :
====================
mult_n_Sm: forall n m : nat, n * m + n = n * S m
====================
An option to clear the output before Search prints its result would be great too.
For the record: there is a button on the RHS of the "select Output" dropdown menu that clears the search manually, but an automatic option one seems like a good idea
@fakusb yes as a matter of fact my usual interaction is that I do a Search then I realise that I can't figure out where the output start. So I do a clean and redo the Search :-(