Def Mathlib.Tactic.getDSimpArgs

Modification history

2023-06-02 06:13
Mathlib/Tactic/Core.lean
fix: spacing and indentation in tactic formatters (#4519) …
Added Mathlib.Tactic.getDSimpArgsView on Github →