Zulip Chat Archive

Stream: general

Topic: How does cc work?

Bryan Gin-ge Chen (Mar 09 2021 at 18:29):

Following a suggestion of @Joseph Myers in #6469, I've been playing around with refactoring boolean_algebra so that it extends a "generalized boolean algebra" class (basically, Boolean algebras which may not have \top, e.g. finset a for a not necessarily fintype) in branch#symm_diff_generalized_boolean_algebra.

However, some proofs by cc have been breaking, e.g. finset.filter_ne and sym2.is_diag_iff_proj_eq. So far I've been able to fix them, but I want to make sure I haven't made some poor decision with the way that I'm structuring the classes. Does cc rely on certain definitional equalities to work or is there something else that I changed that's the culprit?

Last updated: Aug 03 2023 at 10:10 UTC