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
finset a for
a not necessarily
fintype) in branch#symm_diff_generalized_boolean_algebra.
However, some proofs by
cc have been breaking, e.g.
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