mathematics_in_lean_source icon indicating copy to clipboard operation
mathematics_in_lean_source copied to clipboard

Published 20 hours ago • verified publisher icon avigad

rintros ⟨⟩

Open PatrickMassot opened this issue 4 years ago • 1 comments

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

PatrickMassot avatar Jul 03 '20 16:07 PatrickMassot

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 avatar Jul 08 '20 23:07 avigad

Done!

avigad avatar Jul 19 '23 19:07 avigad