Commit 2024-05-21 12:14 7ef3ea2a

View on Github →

feat: port cc tactic (3/3) (#5938) https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/cc.20tactic.20comes.20to.20Lean4

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/CC.lean

added def Lean.MVarId.cc

added def Mathlib.Tactic.CC.CCState.add

added def Mathlib.Tactic.CC.CCState.eqcOf

added def Mathlib.Tactic.CC.CCState.eqcSize

added def Mathlib.Tactic.CC.CCState.eqvProof

added def Mathlib.Tactic.CC.CCState.foldEqc

added def Mathlib.Tactic.CC.CCState.foldEqcM

added def Mathlib.Tactic.CC.CCState.incGMT

added def Mathlib.Tactic.CC.CCState.internalize

added def Mathlib.Tactic.CC.CCState.isEqv

added def Mathlib.Tactic.CC.CCState.isNotEqv

added def Mathlib.Tactic.CC.CCState.mkCore

added def Mathlib.Tactic.CC.CCState.mkUsingHs

added def Mathlib.Tactic.CC.CCState.mkUsingHsCore

added def Mathlib.Tactic.CC.CCState.proofFor

added def Mathlib.Tactic.CC.CCState.proofForFalse

added def Mathlib.Tactic.CC.CCState.refutationFor

added def Mathlib.Tactic.CC.CCState.roots

added def Mathlib.Tactic.CC.CCState.rootsCore

Created test/cc.lean

added inductive Foo

added def Rel

added inductive Vec

added theorem ex₁

added def ex₂

added def foo

added def mul'