Def Mathlib.Tactic.getWithArgs

Modification history

2023-06-02 06:13

Mathlib/Tactic/Core.lean

fix: spacing and indentation in tactic formatters (#4519) …

Added Mathlib.Tactic.getWithArgs View on Github →