Commit 2021-05-10 06:38 8464abab

View on Github →

feat(Tactic/Split): add split tactic

Estimated changes

Modified Mathlib/Data/Nat/Basic.lean

Modified Mathlib/Tactic/Basic.lean

Created Mathlib/Tactic/Split.lean

added def Lean.Elab.Tactic.evalSplit

added def Lean.Meta.split