Def Lean.Elab.Tactic.focusAndBlock

Modification history

2021-10-05 16:47
Mathlib/Tactic/Block.lean
chore: remove block tactic (#58) …
Deleted Lean.Elab.Tactic.focusAndBlockView on Github →
2021-05-10 15:48
Mathlib/Tactic/Block.lean
feat(Tactic/Block): block structuring tactic
Added Lean.Elab.Tactic.focusAndBlockView on Github →