Zulip Chat Archive
Stream: general
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: Dec 20 2023 at 11:08 UTC