Zulip Chat Archive

Stream: general

Topic: Infoview variable grouping

Yaël Dillies (Mar 28 2021 at 21:19):

Imagine you have a bunch of objects of the same type in a proof or a bunch of similar hypotheses, but they aren't grouped in the infoview because they weren't introduced simultaneously. Is there/would it be possible to write a tactic that could untangle this mess at will? Or even better, is it possible to change the infoview so that it automatically groups terms of the same type together? I can't see a reason why you would want to keep them apart.

Eric Wieser (Mar 28 2021 at 21:23):

Dependent variables always appear after the variables they depend on in the current infoview

Eric Wieser (Mar 28 2021 at 21:23):

But otherwise you can revert then intro in a different order

Last updated: Dec 20 2023 at 11:08 UTC