Doc: "Multiplicities" section roadmap

[foxyseta]

https://github.com/idris-lang/Idris2/blob/1dc7b74e4e4b869ef46f73c0f52cadecc88e6f6d/docs/source/tutorial/multiplicities.rst?plain=1#L60

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?

[buzden]

Is this intentional, as "Erasure" is mentioned to still be the most important topic?

I don't quite understand the question, but erasure (i.e. quantity 0) is definitely the most important and most used non-default multiplicity value.

[foxyseta]

Sorry, was too concise to begin with. The doc goes like this:

"In this section, we'll talk about:

• A
• B
• C"

* 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.

[buzden]

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.

[foxyseta]

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.

[foxyseta]

bump

[gallais]

So it makes sense to me to take that as the author's intent.

Yep.

[foxyseta]

Shouldn't linearity appear before erasure in the table of contents, then, as it is tackled first?