About this documentation

This documentation is organised using the following principles.

• Documentation is organised according to the Diátaxis Framework with clear distinction between several parts according to the goals of learning, solving particular problems, referencing during programming and understanding the library. You can watch a wonderful talk by Daniele Procida about such documentation organisation.

• Documentation technically uses Sphinx. All material is written in reStructuredTest and MyST markdown dialect.

• All sections of the documentation containing compilable code are meant to be written in literate Idris.

  • These parts are tested to be built successfully against the current state of the library.

  • Markdown mode of literate Idris is used because it is the only common format supported both by Sphinx and Idris.

  • Only code blocks are checked during this test, inline snippets like the (Vect 3 Nat) [1, 2, 3] are not checked.

  • Although, small letter filenames are meant to be used, fully qualified module name (if used) should use capitalised names, as Idris would expect, There is some machinery that capitalises file and directory names during docs testing. You can look at this section for the example.

This documentation is likely to be not yet full. There are a lot of places still to be filled. You can look at the list of places that are marked as “todos” here.