The State of Idris documentation

Documentation for idris2 is sparse and hard to find, it is sometimes completely missing. This page aims to list and track missing parts of the documentation and additional documents we want to provide for newcomers and for programmers getting stuck in their work.

Existing documentation:

• https://idris2.readthedocs.io/en/latest/ - see "Resources" wiki
• the library Generated HTTP documentation - see "Resources" wiki
• https://www.manning.com/books/type-driven-development-with-idris - see "Resources" wiki

Existing tutorials:

• Functional programming in idris2 - see "Resources" wiki
• Learn idris
• The cookbook

Documentation we wish we had:

Note

The documentation has a separate issue tracker here

• a FAQ - see https://idris2.readthedocs.io/en/latest/faq/faq.html
• a BNF grammar defining Idris language syntax
• a tutorial on quantities - see https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html
• documentation on how to set up interactive editing
• a tutorial that does not require Haskell knowledge - @joelberkeley asks do any of them need Haskell knowledge? I don't know Haskell but haven't found a tutorial I don't understand.
• a tutorial for writing servers and using network primitives
• a tutorial for low level programming and FFI
• a tutorial for how to use the REPL and its commands - see https://idris.readthedocs.io/en/latest/reference/repl.html
• More recipes for the cookbook:
  • make HTTP requests
  • write command line programs
  • connect to a database