Merge pull request #3590 from justjoheinz/patch-3
Provide an example of idris example
commit327d2f0549025f012b7eeac2c9a4efa598c31ab0
authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com>
dateWed 21 Dec 2016, 20:25 (10 years ago)
parentad1343876e0282
docs/reference/documenting.rst+8−1
@@ -61,7 +61,14 @@ italics correctly). A comprehensive set of examples is given below.
6161 ||| Add some numbers.
6262 |||
6363 ||| Addition is really great. This paragraph is not part of the overview.
64− ||| Still the same paragraph. Lists are also nifty:
64+ ||| Still the same paragraph.
65+ |||
66+ ||| You can even provide examples which are inlined in the documentation:
67+ ||| ```idris example
68+ ||| add 4 5
69+ ||| ```
70+ |||
71+ ||| Lists are also nifty:
6572 ||| * Really nifty!
6673 ||| * Yep!
6774 ||| * The name `add` is a **bold** choice