gcongr doc

Stream: mathlib4

[Patrick Massot]

@Mario Carneiro or @Heather Macbeth, could you tell me what docs#Lean.MVarId.gcongr returns? The docstring has a description of the inputs but no description of the outputs.

[Patrick Massot]

It looks like the first output is a success flag and the last argument is a list of created side goals, but the middle one is completely mysterious.

[Patrick Massot]

Just as mysterious as the names input actually.

[Kyle Miller]

It seems to be the with clause names, and it returns the unused ones?

[Patrick Massot]

Thanks, I forgot the existence of this with syntax.

[Heather Macbeth]

Patrick Massot said:

It looks like the first output is a success flag and the last argument is a list of created side goals, but the middle one is completely mysterious.

@Patrick Massot I had to refresh my memory here too, so I hope I will not say anything wrong, but I believe the first output is a "progress" flag (it records "success" in the sense of whether the tactic did anything at all) and the last argument is a list of created goals (both "side" and unresolved "main"). And I believe Kyle's explanation is correct for the middle goal.

[Patrick Massot]

Thanks!