Provide an example of idris example
The documentation reference lacked an example of using idris example to document code.
commit76e028223bbe79bcd226b8dd510ec9b4332a88f8
authorMarkus Klink <justjoheinz@gmail.com>
dateWed 21 Dec 2016, 14:24 (10 years ago)
parentad13438
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