doc: mention x:h@e variant in docstring of x@e
#3073
Conversation
This was done in 1c1e6d7
|
Thanks! BTW, in this repo, the PR description becomes the commit message, so if you remove empty |
Head branch was pushed to by a user without write access
|
Perhaps the PR template should make that obvious; I thought I was expected to leave the heading, since the template added it for me! |
| /-- `x@e` or `x:h@e` matches the pattern `e` and binds its value to the identifier `x`. | ||
| If present, the identifier `h` is bound to a proof of `x = e`. -/ |
There was a problem hiding this comment.
@nomeata, I pushed this docstring too
I guess the heading wouldn’t hurt if actual content followed it :-). But yes, the commit-from-pr-description workflow seems to work nicely, so I should refine the template. |
|
Would you find the phrasing in #3074 more helpful? Feel free to suggest improvements over there. |
nomeata
changed the title
x:h@e variant in docstring of x@e
This was done in 1c1e6d7
Zulip thread