Commit 2024-06-23 23:52 bff23e15

View on Github →

chore: restore cc tactic (#13404) The cc tactic is a high-cost tactic, so I restored cc tactics only if a proof can be reduced significantly. I made sure that cc tactic works on in the all changed proofs except when the other specification changes in Lean 4 changes a goal.

Estimated changes