upstream Std.Lean.Delaborator

Stream: batteries

[Kim Morrison]

@Mario Carneiro, any objections to upstreaming Lean.ppConst from Std.Lean.Delaborator? The rw? tactic should be using it (via TryThis.addRewriteSuggestion). If there's any where else you know it should be used upstreamed I can try to include those at the same time.

[Mario Carneiro]

No objections. Looking at uses of .ofPPFormat in std I also see some cases where we want a version of ppSignature which produces a message data (and possibly linking the constant); it would be nice to not ever have to write .ofPPFormat in usage code and upstream what we need to make the existing cases in std / mathlib work

[Mario Carneiro]

looks like elabCheckCore in core also has a use of .ofPPFormat

[Mario Carneiro]

oh in fact it's a buggy use, it should really have tagAppFn enabled like the analogous use of ppSignature in std

[Mario Carneiro]

which strengthens the argument for having a dedicated function for it

[Mario Carneiro]

(In general, I think we should treat anything in the Std.Lean subfolder as "approved for moving upstream", because it is explicitly intended as a staging ground for such move)

[Kim Morrison]

@Mario Carneiro, is lean4#3911 close enough to what you had in mind here?