Doc: "Multiplicities" section roadmap about idris2

[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?