Commit 2021-10-14 09:04 60afa55e

View on Github →

chore: remove split tactic (#70) https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Renaming.20.60split.60

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

added theorem List.mem_constructor

deleted theorem List.mem_split

Modified Mathlib/Data/List/Card.lean

Modified Mathlib/Init/Data/Nat/Lemmas.lean

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Tactic/Basic.lean

Deleted Mathlib/Tactic/Split.lean

deleted def Lean.Meta.split

Modified test/Split.lean

Modified test/basicTactics.lean

Modified test/showTerm.lean