rintros ⟨⟩

[PatrickMassot]

Do we want to explain the rintros ⟨⟩ trick somewhere?

[avigad]

It just guesses the pattern, right, and chooses its own names? I guess that is useful when the user doesn't have to look at the names, e.g, when automation will work? Is there a compelling example at this point, or should we wait until we have one?

[avigad]

Done!