leanprover-community/leanprover-community.github.io#174

Stream: PR reviews

[Eric Wieser]

Since we don't seem to have this syntax documented anywhere, it would be nice to get some version of this merged. I think I've addressed @Mario Carneiro worries with the first revision, but its easy to forget PRs in non-mathlib repos