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