Commit 2021-05-10 15:48 8ced11cf

View on Github →

feat(Tactic/Block): block structuring tactic

Estimated changes

Modified Mathlib/Data/Nat/Basic.lean

Modified Mathlib/Tactic/Basic.lean

Created Mathlib/Tactic/Block.lean

added def Lean.Elab.Tactic.closeAllOrAdmit

added def Lean.Elab.Tactic.focusAndBlock

Modified Mathlib/Tactic/NoMatch.lean

Modified Mathlib/Tactic/Split.lean

deleted def Lean.Elab.Tactic.evalSplit