Def Lean.Parser.Tactic.getUsingArg

Modification history

2023-06-02 06:13
Mathlib/Tactic/Core.lean
fix: spacing and indentation in tactic formatters (#4519) …
Deleted Lean.Parser.Tactic.getUsingArgView on Github →
2022-03-14 18:42
Mathlib/Tactic/Core.lean
feat : `simpa` tactic (#224)
Added Lean.Parser.Tactic.getUsingArgView on Github →