idris-lang/Idris-dev — pull request #1613 by david-christiansen (2014-10-10 05:36:40+00:00)
Title: Add syntax for example code to docs

Now, code defined with the "example" Markdown attribute will be rendered
as an inline REPL-style example. For instance:
``````
```` idris example
with List (reverse ["a", "b", "c"])
````
``````

renders to

> reverse ["a", "b", "c"]
["c", "b", "a"]