Topic: filter Lean messages
Patrick Massot (Aug 08 2018 at 11:26):
@Gabriel Ebner it would be nice to add a button next to the "Updating/Stopped" toggle which would allow filtering out certain context lines, especially everything starting with
_inst_. Because of mixin classes, I currently work on a proof whose starting context goes up to
_inst_24. Very quickly I need to scroll down to see the current goal...
Patrick Massot (Aug 08 2018 at 16:53):
An even more aggressive option would be to also filter out
.* : Type .*
Patrick Massot (Aug 08 2018 at 16:54):
We could have a toggle cycling between default (show every line), filter out instances, filter out instances and types.
Last updated: Aug 03 2023 at 10:10 UTC