Commit 2023-06-02 06:13 162ec819
View on Github →fix: spacing and indentation in tactic formatters (#4519) This fixes a bunch of spacing bugs in tactics. Mathlib counterpart of:
fix: spacing and indentation in tactic formatters (#4519) This fixes a bunch of spacing bugs in tactics. Mathlib counterpart of: