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:

  • Lean: leanprover/lean4#2240
  • Std: leanprover/std4#149
  • Aesop: JLimperg/aesop#56

Estimated changes

modified def Set.image
modified def Set.powerset