EQUATION_EXPLORER: Give an option in equation explorer to allow the "expanded" list of equations beyond the original 4694

[teorth]

See https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Equation.205105.20-.3E.20Equation.202 for discussion. By default one should restrict attention to the "Core" graph of the initial 4694 equations.

[teorth]

This may require first resolving #142.

[vlad902]

Some of our workflows depend on the sporadic equations not being included in the list of 'not fully solved equations'. It would probably require yet-another checkbox to filter them out to maintain those workflows, unless there's another method I'm not thinking of.

[teorth]

Yeah, it requires yet another checkbox, and they should filtered out by default. We're beginning to have quite a few of these checkboxes, but they're all independently useful so I don't see any better thing to do than just have all of the options available.

[Osalotioman]

claim

[Osalotioman]

Zulip Thread