-
Notifications
You must be signed in to change notification settings - Fork 366
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: "Multiplicities" section roadmap #3264
Comments
I don't quite understand the question, but erasure (i.e. quantity |
Sorry, was too concise to begin with. The doc goes like this: "In this section, we'll talk about:
* proceeds to talk about B first, A later, C last. * So I thought maybe this was not intentional and you would like to be consistent in the order the topics are mentioned/covered? If not, my bad. |
I agree that it would be more logical to have sections in the order "A, B, C", as in the prefix. I don't know exactly about intentions of the original documentation writer, but I'm sure it's okay to propose reordering of the sections. |
At some point there is an explicit declaration of intent along the lines of: "The most interesting, however, and the thing which gives Idris 2 much more expressivity, is linearity, so we'll start there." So it makes sense to me to take that as the author's intent. |
Idris2/docs/source/tutorial/multiplicities.rst
Line 60 in 1dc7b74
The topics that are about to be covered are not listed in the right order. Is this intentional, as "Erasure" is mentioned to still be the most important topic?
The text was updated successfully, but these errors were encountered: