07ee064a9a
* Expands on documentation of the 'with' rule This additional text clarifies the syntax of the 'with' rule: - it gives the name "view refined argument pattern" to argument patterns to the left of the | vertical bar. - it explains that when the original function argument patterns are unchanged, then the refined pattern may be omitted, using the 'filter' function as an example. - it decomposes in a bit more detail the body of the 'natToBin' function, explaining in bullet point form where the refined patterns have come from, i.e. Even and Odd constructor definitions. |
||
|---|---|---|
| .. | ||
| effects | ||
| faq | ||
| guides | ||
| image | ||
| listing | ||
| proofs | ||
| reference | ||
| st | ||
| tutorial | ||
| .gitignore | ||
| conf.py | ||
| index.rst | ||
| LICENSE | ||
| make.bat | ||
| Makefile | ||
| README.md | ||
Documentation for the Idris Language.
This manual has been prepared using ReStructured Text and the Sphinx Documentation Generator for future inclusion on Read The Docs.
Dependencies
To build the manual the following dependencies must be met. We assume that you have standard build automation tools already install i.e. make.
Sphinx-Doc
Python should be installed by default on most systems. Sphinx can be installed either through your hosts package manager or using pip/easy_install.
Note ReadTheDocs works with Sphinx
v1.2.2. If you install a more recent version of sphinx then
'incorrectly' marked up documentation may get passed the build system
of readthedocs and be ignored. In the past we had several code-blocks
disappear because of that.
The ReadTheDocs theme can be installed using pip as follows:
pip install sphinx_rtd_theme
LaTeX
LaTeX can be install either using your systems package manager or direct from TeXLive.
Build Instructions
make html
make latexpdf
Contributing
The documentation for Idris has been published under the Creative Commons CC0 License. As such to the extent possible under law, /The Idris Community/ has waived all copyright and related or neighboring rights to Documentation for Idris.
More information concerning the CC0 can be found online at:
http://creativecommons.org/publicdomain/zero/1.0/
When contributing material to the manual please bear in mind that the work will be licensed as above.