Commit 2026-02-01 13:22 cb84f90f

View on Github →

chore: move cc to another repository (#34669) cc tactic is replaced by grind and deprecated since 2025-07-31, so I created the repository Komyyy/legacy-cc and move cc tactic to there.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Deleted Mathlib/Tactic/CC.lean

deleted def Lean.MVarId.cc

deleted def Mathlib.Tactic.CC.CCState.add

deleted def Mathlib.Tactic.CC.CCState.eqcOf

deleted def Mathlib.Tactic.CC.CCState.eqcSize

deleted def Mathlib.Tactic.CC.CCState.eqvProof

deleted def Mathlib.Tactic.CC.CCState.foldEqc

deleted def Mathlib.Tactic.CC.CCState.foldEqcM

deleted def Mathlib.Tactic.CC.CCState.incGMT

deleted def Mathlib.Tactic.CC.CCState.internalize

deleted def Mathlib.Tactic.CC.CCState.isEqv

deleted def Mathlib.Tactic.CC.CCState.isNotEqv

deleted def Mathlib.Tactic.CC.CCState.mkCore

deleted def Mathlib.Tactic.CC.CCState.mkUsingHs

deleted def Mathlib.Tactic.CC.CCState.mkUsingHsCore

deleted def Mathlib.Tactic.CC.CCState.proofFor

deleted def Mathlib.Tactic.CC.CCState.proofForFalse

deleted def Mathlib.Tactic.CC.CCState.refutationFor

deleted def Mathlib.Tactic.CC.CCState.roots

deleted def Mathlib.Tactic.CC.CCState.rootsCore

Deleted Mathlib/Tactic/CC/Addition.lean

deleted def Mathlib.Tactic.CC.CCM.add

deleted def Mathlib.Tactic.CC.CCM.addACEq

deleted def Mathlib.Tactic.CC.CCM.addCongruenceTable

deleted def Mathlib.Tactic.CC.CCM.addEqvCore

deleted def Mathlib.Tactic.CC.CCM.addEqvStep

deleted def Mathlib.Tactic.CC.CCM.addOccurrence

deleted def Mathlib.Tactic.CC.CCM.addSymmCongruenceTable

deleted def Mathlib.Tactic.CC.CCM.checkEqTrue

deleted def Mathlib.Tactic.CC.CCM.checkInvariant

deleted def Mathlib.Tactic.CC.CCM.checkNewSubsingletonEq

deleted def Mathlib.Tactic.CC.CCM.collapseAC

deleted def Mathlib.Tactic.CC.CCM.collectFnRoots

deleted def Mathlib.Tactic.CC.CCM.compareSymm

deleted def Mathlib.Tactic.CC.CCM.compareSymmAux

deleted def Mathlib.Tactic.CC.CCM.composeAC

deleted def Mathlib.Tactic.CC.CCM.dbgTraceACEq

deleted def Mathlib.Tactic.CC.CCM.dbgTraceACState

deleted def Mathlib.Tactic.CC.CCM.eraseRBHSOccs

deleted def Mathlib.Tactic.CC.CCM.eraseROccs

deleted def Mathlib.Tactic.CC.CCM.eraseRRHSOccs

deleted def Mathlib.Tactic.CC.CCM.getACTodo

deleted def Mathlib.Tactic.CC.CCM.getEqcLambdas

deleted def Mathlib.Tactic.CC.CCM.getTodo

deleted def Mathlib.Tactic.CC.CCM.insertEraseROcc

deleted def Mathlib.Tactic.CC.CCM.insertEraseROccs

deleted def Mathlib.Tactic.CC.CCM.insertRBHSOccs

deleted def Mathlib.Tactic.CC.CCM.insertROccs

deleted def Mathlib.Tactic.CC.CCM.insertRRHSOccs

deleted def Mathlib.Tactic.CC.CCM.internalize

deleted def Mathlib.Tactic.CC.CCM.internalizeAC

deleted def Mathlib.Tactic.CC.CCM.internalizeACVar

deleted def Mathlib.Tactic.CC.CCM.isAC

deleted def Mathlib.Tactic.CC.CCM.mayPropagate

deleted def Mathlib.Tactic.CC.CCM.mkACSuperposeProof

deleted def Mathlib.Tactic.CC.CCM.mkCongruencesKey

deleted def Mathlib.Tactic.CC.CCM.mkSymmCongruencesKey

deleted def Mathlib.Tactic.CC.CCM.modifyACTodo

deleted def Mathlib.Tactic.CC.CCM.modifyTodo

deleted def Mathlib.Tactic.CC.CCM.processAC

deleted def Mathlib.Tactic.CC.CCM.processTodo

deleted def Mathlib.Tactic.CC.CCM.propagateAndDown

deleted def Mathlib.Tactic.CC.CCM.propagateBeta

deleted def Mathlib.Tactic.CC.CCM.propagateBetaToEqc

deleted def Mathlib.Tactic.CC.CCM.propagateDown

deleted def Mathlib.Tactic.CC.CCM.propagateEqDown

deleted def Mathlib.Tactic.CC.CCM.propagateExistsDown

deleted def Mathlib.Tactic.CC.CCM.propagateInstImplicit

deleted def Mathlib.Tactic.CC.CCM.propagateNotDown

deleted def Mathlib.Tactic.CC.CCM.propagateOrDown

deleted def Mathlib.Tactic.CC.CCM.propagateProjectionConstructor

deleted def Mathlib.Tactic.CC.CCM.propagateValueInconsistency

deleted def Mathlib.Tactic.CC.CCM.pushEq

deleted def Mathlib.Tactic.CC.CCM.pushHEq

deleted def Mathlib.Tactic.CC.CCM.pushReflEq

deleted def Mathlib.Tactic.CC.CCM.pushSubsingletonEq

deleted def Mathlib.Tactic.CC.CCM.pushTodo

deleted def Mathlib.Tactic.CC.CCM.reinsertParents

deleted def Mathlib.Tactic.CC.CCM.removeParents

deleted def Mathlib.Tactic.CC.CCM.setACVar

deleted def Mathlib.Tactic.CC.CCM.superposeAC

Deleted Mathlib/Tactic/CC/Datatypes.lean

deleted def Mathlib.Tactic.CC.ACApps.append

deleted def Mathlib.Tactic.CC.ACApps.diff

deleted def Mathlib.Tactic.CC.ACApps.intersection

deleted def Mathlib.Tactic.CC.ACApps.isSubset

deleted def Mathlib.Tactic.CC.ACApps.mkApps

deleted def Mathlib.Tactic.CC.ACApps.mkFlatApps

deleted def Mathlib.Tactic.CC.ACApps.toExpr

deleted inductive Mathlib.Tactic.CC.ACApps

deleted def Mathlib.Tactic.CC.ACEntry.ROccs

deleted structure Mathlib.Tactic.CC.ACEntry

deleted structure Mathlib.Tactic.CC.CCConfig

deleted structure Mathlib.Tactic.CC.CCCongrTheorem

deleted structure Mathlib.Tactic.CC.CCCongrTheoremKey

deleted structure Mathlib.Tactic.CC.CCNormalizer

deleted structure Mathlib.Tactic.CC.CCPropagationHandler

deleted def Mathlib.Tactic.CC.CCState.checkEqc

deleted def Mathlib.Tactic.CC.CCState.checkInvariant

deleted def Mathlib.Tactic.CC.CCState.getNumROccs

deleted def Mathlib.Tactic.CC.CCState.getRoots

deleted def Mathlib.Tactic.CC.CCState.getVarWithLeastLHSOccs

deleted def Mathlib.Tactic.CC.CCState.getVarWithLeastOccs

deleted def Mathlib.Tactic.CC.CCState.getVarWithLeastRHSOccs

deleted def Mathlib.Tactic.CC.CCState.inSingletonEqc

deleted def Mathlib.Tactic.CC.CCState.isCgRoot

deleted def Mathlib.Tactic.CC.CCState.mkEntryCore

deleted def Mathlib.Tactic.CC.CCState.mt

deleted def Mathlib.Tactic.CC.CCState.next

deleted def Mathlib.Tactic.CC.CCState.ppAC

deleted def Mathlib.Tactic.CC.CCState.ppACDecl

deleted def Mathlib.Tactic.CC.CCState.ppACDecls

deleted def Mathlib.Tactic.CC.CCState.ppACExpr

deleted def Mathlib.Tactic.CC.CCState.ppACR

deleted def Mathlib.Tactic.CC.CCState.ppEqc

deleted def Mathlib.Tactic.CC.CCState.ppEqcs

deleted def Mathlib.Tactic.CC.CCState.ppParentOccs

deleted def Mathlib.Tactic.CC.CCState.ppParentOccsAux

deleted def Mathlib.Tactic.CC.CCState.root

deleted structure Mathlib.Tactic.CC.CCState

deleted structure Mathlib.Tactic.CC.CCStructure

deleted inductive Mathlib.Tactic.CC.CongruencesKey

deleted inductive Mathlib.Tactic.CC.DelayedExpr

deleted structure Mathlib.Tactic.CC.Entry

deleted inductive Mathlib.Tactic.CC.EntryExpr

deleted structure Mathlib.Tactic.CC.ParentOcc

deleted structure Mathlib.Tactic.CC.SymmCongruencesKey

deleted def Mathlib.Tactic.CC.isInterpretedValue

deleted def Mathlib.Tactic.CC.isValue

deleted def Mathlib.Tactic.CC.liftFromEq

deleted def Mathlib.Tactic.CC.mkCCHCongrWithArity

Deleted Mathlib/Tactic/CC/Lemmas.lean

deleted theorem Mathlib.Tactic.CC.and_eq_of_eq

deleted theorem Mathlib.Tactic.CC.and_eq_of_eq_false_left

deleted theorem Mathlib.Tactic.CC.and_eq_of_eq_false_right

deleted theorem Mathlib.Tactic.CC.and_eq_of_eq_true_left

deleted theorem Mathlib.Tactic.CC.and_eq_of_eq_true_right

deleted theorem Mathlib.Tactic.CC.eq_false_of_not_eq_true

deleted theorem Mathlib.Tactic.CC.eq_false_of_or_eq_false_left

deleted theorem Mathlib.Tactic.CC.eq_false_of_or_eq_false_right

deleted theorem Mathlib.Tactic.CC.eq_true_of_and_eq_true_left

deleted theorem Mathlib.Tactic.CC.eq_true_of_and_eq_true_right

deleted theorem Mathlib.Tactic.CC.eq_true_of_not_eq_false

deleted theorem Mathlib.Tactic.CC.false_of_a_eq_not_a

deleted theorem Mathlib.Tactic.CC.if_eq_of_eq

deleted theorem Mathlib.Tactic.CC.if_eq_of_eq_false

deleted theorem Mathlib.Tactic.CC.if_eq_of_eq_true

deleted theorem Mathlib.Tactic.CC.iff_eq_of_eq_true_left

deleted theorem Mathlib.Tactic.CC.iff_eq_of_eq_true_right

deleted theorem Mathlib.Tactic.CC.iff_eq_true_of_eq

deleted theorem Mathlib.Tactic.CC.imp_eq_of_eq_false_left

deleted theorem Mathlib.Tactic.CC.imp_eq_of_eq_false_right

deleted theorem Mathlib.Tactic.CC.imp_eq_of_eq_true_left

deleted theorem Mathlib.Tactic.CC.imp_eq_of_eq_true_right

deleted theorem Mathlib.Tactic.CC.imp_eq_true_of_eq

deleted theorem Mathlib.Tactic.CC.not_eq_of_eq_false

deleted theorem Mathlib.Tactic.CC.not_eq_of_eq_true

deleted theorem Mathlib.Tactic.CC.not_imp_eq_of_eq_false_right

deleted theorem Mathlib.Tactic.CC.or_eq_of_eq

deleted theorem Mathlib.Tactic.CC.or_eq_of_eq_false_left

deleted theorem Mathlib.Tactic.CC.or_eq_of_eq_false_right

deleted theorem Mathlib.Tactic.CC.or_eq_of_eq_true_left

deleted theorem Mathlib.Tactic.CC.or_eq_of_eq_true_right

Deleted Mathlib/Tactic/CC/MkProof.lean

deleted def Mathlib.Tactic.CC.CCM.flipDelayedProofCore

deleted def Mathlib.Tactic.CC.CCM.flipProof

deleted def Mathlib.Tactic.CC.CCM.flipProofCore

deleted def Mathlib.Tactic.CC.CCM.getCache

deleted def Mathlib.Tactic.CC.CCM.getEntry

deleted def Mathlib.Tactic.CC.CCM.getEqFalseProof

deleted def Mathlib.Tactic.CC.CCM.getEqTrueProof

deleted def Mathlib.Tactic.CC.CCM.getInconsistencyProof

deleted def Mathlib.Tactic.CC.CCM.getPropEqProof

deleted def Mathlib.Tactic.CC.CCM.getRoot

deleted def Mathlib.Tactic.CC.CCM.hasHEqProofs

deleted def Mathlib.Tactic.CC.CCM.isCgRoot

deleted def Mathlib.Tactic.CC.CCM.isEqFalse

deleted def Mathlib.Tactic.CC.CCM.isEqTrue

deleted def Mathlib.Tactic.CC.CCM.isEqv

deleted def Mathlib.Tactic.CC.CCM.isNotEqv

deleted def Mathlib.Tactic.CC.CCM.mkACProof

deleted def Mathlib.Tactic.CC.CCM.mkACSimpProof

deleted def Mathlib.Tactic.CC.CCM.mkCCCongrTheorem

deleted def Mathlib.Tactic.CC.CCM.mkCCHCongrTheorem

deleted def Mathlib.Tactic.CC.CCM.mkNeOfEqOfNe

deleted def Mathlib.Tactic.CC.CCM.mkNeOfNeOfEq

deleted def Mathlib.Tactic.CC.CCM.mkTrans

deleted def Mathlib.Tactic.CC.CCM.mkTransOpt

deleted def Mathlib.Tactic.CC.CCM.modifyCache

deleted def Mathlib.Tactic.CC.CCM.normalize

deleted def Mathlib.Tactic.CC.CCM.run

deleted def Mathlib.Tactic.CC.CCM.setFO

deleted def Mathlib.Tactic.CC.CCM.simplifyAC

deleted def Mathlib.Tactic.CC.CCM.simplifyACCore

deleted def Mathlib.Tactic.CC.CCM.simplifyACStep

Deleted MathlibTest/cc.lean

deleted inductive Foo

deleted def Rel

deleted inductive Vec

deleted theorem ex₁

deleted def ex₂

deleted def foo

deleted def mul'

Modified scripts/nolints.json

Modified scripts/noshake.json