Def Mathlib.Tactic.getUsingArg

Modification history

2023-06-02 06:13

Mathlib/Tactic/Core.lean

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

Added Mathlib.Tactic.getUsingArg View on Github →