Alternative "toMessageData" for a list

Stream: metaprogramming / tactics

[Heather Macbeth]

I want to print a list of Expr in an error message of a tactic, see PR review. Currently my tactic code says

throwError "The steps which could not be automatically justified were: {g}"

and the output looks like

 The steps which could not be automatically justified were: [0 ≤
   x,
 c ≤ d]

Questions:

• how do I specify options for the printing of the list? I'd like it to be printed as "l1 [linebreak] l2 [linebreak] ..." rather than "[l1, l2, l3]", so different separating, beginning and end characters
• what's with the linebreak when the error message prints the 0 ≤ x expression?

[Heather Macbeth]

In context:
https://github.com/leanprover-community/mathlib4/blob/1d06bf7ec1fb0ca60b0f382186bb3cca36911ba6/Mathlib/Tactic/RelCongr/Core.lean#L505

[Eric Wieser]

docs4#Lean.MessageData.ofList ?

[Heather Macbeth]

That looks nice -- I see it does

Write the given list of messages as a list, separating each item with ,\n and surrounding with square brackets.

is there a way to vary this (I don't want the square brackets, and would prefer not to have the commas either)?

[Heather Macbeth]

Note that I think the method you pointed me to is the one that's already being used in the output by default.

[Eric Wieser]

The implementation is pretty simple; I would guess you could just inline a version of it for what you actually want

[Heather Macbeth]

For the record, the function I was after does exist (and is actually called in the implementation of the default toMessageData): it is docs4#Lean.MessageData.joinSep.