Menu
▾
▴
#401 Hide/deselect more equalities after rewriting
In [feature-requests:#371], we were asked to hide equalities after rewriting them. At the time, it was decided that this should only be done when the rewritten expression is a single variable.
It seems that this was too restrictive. We can apply the same logic to the rewriting of an arbitrarily complex expression, as long as none of its free identifiers are used in other hypotheses.
This should be implemented with [bugs:#818] in mind: the rewritten hypothesis should be either deselected or hidden depending on whether its free identifiers appear in the default (visible but not selected) hypotheses or not.
Related
