Def Lean.Parser.Tactic.getDSimpArgs

Modification history

2023-06-02 06:13
Mathlib/Tactic/Core.lean
fix: spacing and indentation in tactic formatters (#4519) …
Deleted Lean.Parser.Tactic.getDSimpArgsView on Github →
2022-09-15 04:19
Mathlib/Tactic/Core.lean
chore: simp `with` clauses are no longer needed (#409) …
Added Lean.Parser.Tactic.getDSimpArgsView on Github →