Commit 2024-12-18 11:06 b7666b88

View on Github →

chore(Mathlib/Tactic/CC/Addition): split a file (#19989)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/CC/Addition.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

Modified Mathlib/Tactic/CC/Datatypes.lean

Created Mathlib/Tactic/CC/MkProof.lean

added def Mathlib.Tactic.CC.CCM.flipDelayedProofCore

added def Mathlib.Tactic.CC.CCM.flipProof

added def Mathlib.Tactic.CC.CCM.flipProofCore

added def Mathlib.Tactic.CC.CCM.getCache

added def Mathlib.Tactic.CC.CCM.getEntry

added def Mathlib.Tactic.CC.CCM.getEqFalseProof

added def Mathlib.Tactic.CC.CCM.getEqTrueProof

added def Mathlib.Tactic.CC.CCM.getInconsistencyProof

added def Mathlib.Tactic.CC.CCM.getPropEqProof

added def Mathlib.Tactic.CC.CCM.getRoot

added def Mathlib.Tactic.CC.CCM.hasHEqProofs

added def Mathlib.Tactic.CC.CCM.isCgRoot

added def Mathlib.Tactic.CC.CCM.isEqFalse

added def Mathlib.Tactic.CC.CCM.isEqTrue

added def Mathlib.Tactic.CC.CCM.isEqv

added def Mathlib.Tactic.CC.CCM.isNotEqv

added def Mathlib.Tactic.CC.CCM.mkACProof

added def Mathlib.Tactic.CC.CCM.mkACSimpProof

added def Mathlib.Tactic.CC.CCM.mkCCCongrTheorem

added def Mathlib.Tactic.CC.CCM.mkCCHCongrTheorem

added def Mathlib.Tactic.CC.CCM.mkNeOfEqOfNe

added def Mathlib.Tactic.CC.CCM.mkNeOfNeOfEq

added def Mathlib.Tactic.CC.CCM.mkTrans

added def Mathlib.Tactic.CC.CCM.mkTransOpt

added def Mathlib.Tactic.CC.CCM.modifyCache

added def Mathlib.Tactic.CC.CCM.normalize

added def Mathlib.Tactic.CC.CCM.run

added def Mathlib.Tactic.CC.CCM.setFO

added def Mathlib.Tactic.CC.CCM.simplifyAC

added def Mathlib.Tactic.CC.CCM.simplifyACCore

added def Mathlib.Tactic.CC.CCM.simplifyACStep

Modified scripts/noshake.json