@@ -33,6 +33,30 @@ for use in production would be very welcome - this includes (but is not
3333limited to) extra library support, polishing the run-time system (and ensuring
3434it is robust), providing and maintaining a JVM back end, etc.
3535
36+Is there some documentation for the standard lib? List of functions?
37+=====================================================================
38+
39+API documentation for the shipped packages is listed on `the
40+documentation page <http://www.idris-lang.org/documentation/>`_.
41+
42+Unfortunately, the default prelude and shipped packages for `Idris`
43+are not necessarily complete with regards to documentation. Other
44+ways to find functions include:
45+
46++ REPL commands:
47+
48+ + Use `:apropos` to search for text in documentation and function names.
49+ + Use `:search` to search for functions of a given type.
50+ + Use `:browse` to list the contents of a given namespace.
51+
52++ Use the REPL's auto-complete functionality.
53++ Grep through the source code in `libs/`
54+
55+If you find that the shipped packages are lacking in documentation,
56+please feel free to write some. Or bug someone to do so. `Idris` has
57+syntax for providing rich documentation, which is then viewable using
58+the `:doc` command and listed in generated HTML API documentation.
59+
3660
3761Why does Idris use eager evaluation rather than lazy?
3862=====================================================
@@ -191,10 +215,10 @@ function.
191215When will Idris be self-hosting?
192216================================
193217
194−It’s not a priority, though not a bad idea in the long run. It would be a
195−worthwhile effort in the short term to implement libraries to support
196−self-hosting, such as a good parsing library.
197−
218+It’s not a priority, though not a bad idea in the long run. It would
219+be a worthwhile effort in the short term to implement libraries in
220+Idris to support self-hosting, such as argument parsing and a
221+POSIX-compliant library for system interaction.
198222
199223Does Idris have universe polymorphism? What is the type of ``Type``?
200224====================================================================