I think this example (provided by Emilio Jesús Gallego Arias) might be added to the first part of book where examples of [:: 1; 2] notation are given. I think one needs to give signature of tnth and small description of what does it do and mention that explanation is in the second part of the book. I think it is rather easy to get the idea of how this notation can be used when discussing notations.
Eval compute in tnth [tuple 1; 2; 3] (sub_ord 1).I think this example (provided by Emilio Jesús Gallego Arias) might be added to the first part of book where examples of
[:: 1; 2]notation are given. I think one needs to give signature oftnthand small description of what does it do and mention that explanation is in the second part of the book. I think it is rather easy to get the idea of how this notation can be used when discussing notations.Related issue https://github.com/math-comp/mcb/issues/127