custom `pretty_cases`

Stream: general

[Kayla Thomas]

Is there a way to customize the result of the pretty_cases tactic? For example, to change the way the variable names are generated and the formatting of the { admit }?

[Kayla Thomas]

I guess I would need to change the source here for the latter: https://github.com/leanprover-community/mathlib/blob/bd835ef554f37ef9b804f0903089211f89cb370b/src/tactic/pretty_cases.lean#L56