Doc: "Multiplicities" section roadmap

[foxyseta]

Idris2/docs/source/tutorial/multiplicities.rst

Line 60 in 1dc7b74

* :ref:`sect-erasure` - how to know what is relevant at run time and what is erased

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?