-
Notifications
You must be signed in to change notification settings - Fork 350
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
doc: Improve docstrings around Array.mk,.data,.toList #2771
Conversation
|
On Zulip there was some disagreement which function should be recommended to be used, without conclusion. To not have this PR (which makes no such recommendation either way) sitting around for much longer, I’ll merge it if noone complains. Further improvements are still possible of course. |
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@digama0 do you overall agree with these changes? |
Regarding the main question, my opinion is as mentioned on zulip - we should rename |
following a discussion at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Understanding.20the.20docstring.20for.20docs.23Array.2Edata/near/398705430