Pretty-printing an arbitrary list [x_1, ... x_n] using a value printer f as: [[f(x_1)], ..., [f(x_n)]]
alpha_to_string
a value printer
l
a list to be pretty-printed.NB: this is the default list-printer
Markdown Syntax Help
You can enter a message using a Markdown-like syntax. Here is a list of all elements recognized.
Paragraph
A group of text isolated by two or more linebreaks will be put in a HTML paragraph <p>.
Titles
You can enter titles using various syntax:
First level title =================
will create:
First level title
and
Second level title ------------------
will create:
Second level title
You can also create titles by preceding text with as many # as the
level of the title, so
#### Title 4
will create:
Title 4
Emphasis
You may want to put emphasis on some words in your texts.
You can do a simple emphasis by surrounding some text with
* or _: *text* will give in result *text*.
To put a strong emphasis on something, you can surround it with
** or __: __text__ will give in result text.
You can put *a **strong emphasis** inside a simple one* or __a _simple emphasis_ inside a strong one__.
Lists
You can insert simple bullet lists simply by putting each element in
a line starting by a -, a + or a *. Mixing symbols will not create
different lists unless there is a blank line in the middle:
- one - two
* three + four
will result in:
- one
- two
- three
- four
If you want to put a linebreak in your source to avoid very long lines, you can put four spaces or a tabulation at the beginning of your line to keep the content as one list element:
- one
two
- three
four
will result in:
- one two
- three four
To insert numbered lists, you can follow the same rules and start your lines with a number followed by a period. The numbers do not have to follow a logical suit to be recognized:
1. one
two
3. three
42. four
444. five
will result in:
- one two
- three
- four
- five
Links
You can insert links inside your text in two ways:
some text [Inline-style](https://mlstate.com "MLstate") more text or some text [Reference-style][mlstate] some random text [mlstate]: https://mlstate.com "MLstate"
In both cases, the title ("MLstate") is optional. The result of the above is:
some text Inline-style more text or some text Reference-style some random text
Note that references are case-sensitive and can be used for several links.
Images
Image insertion uses the same syntax than inserting links preceded by a !:
 ![HTML5][html5] [html5]: http://www.w3.org/html/logo/badge/html5-badge-h-solo.png "HTML5"
both result in:
You can use the same reference for a link and an image (referencing the same URL).
Code
There are two ways of inserting code inside your text.
Firstly, you can surround it with `, so `some code` will
result in some code.
You can also indent a paragraph with at least four spaces or a tabulation:
rec fact(x) =
if x < 1 then 1
else x * fact(x-1)
will result in:
rec fact(x) = if x < 1 then 1 else x * fact(x-1)
Quote
You can insert a quote in you texts by preceding it with >. You
can put a quote inside a quote:
> > An indented quote > A standard quote
will result in:
An indented quote
A standard quote
Other
You can insert an html line break (<br/>) by putting two spaces at
the end of the line.
You can insert a horizontal line by writing a line containing only
the character - preceded by an empty line (otherwise it would result
in a second-level header).
-------------- Some text with a linebreak
will result in:
Some text with a linebreak
You can enter a message using a Markdown-like syntax.
Here is a list of all elements recognized.
## Paragraph
A group of text isolated by two or more linebreaks will be put
in a HTML paragraph <p>.
## Titles
You can enter titles using various syntax:
First level title
=================
will create:
First level title
=================
and
Second level title
------------------
will create:
Second level title
-----------------
You can also create titles by preceding text with as many `#` as the
level of the title, so
#### Title 4
will create:
#### Title 4
## Emphasis
You may want to put emphasis on some words in your texts.
You can do a *simple emphasis* by surrounding some text with
`*` or `_`: `*text*` will give in result *text*.
To put a **strong emphasis** on something, you can surround it with
`**` or `__`: `__text__` will give in result __text__.
You can put *a **strong emphasis** inside a simple one* or
__a _simple emphasis_ inside a strong one__.
## Lists
You can insert simple bullet lists simply by putting each element in
a line starting by a `-`, a `+` or a `*`. Mixing symbols will not create
different lists unless there is a blank line in the middle:
- one
- two
* three
+ four
will result in:
- one
- two
* three
+ four
If you want to put a linebreak in your source to avoid very long lines, you
can put four spaces or a tabulation at the beginning of your line to keep the
content as one list element:
- one
two
- three
four
will result in:
- one
two
- three
four
To insert numbered lists, you can follow the same rules and start your lines
with a number followed by a period. The numbers do not have to follow a logical
suit to be recognized:
1. one
two
3. three
42. four
444. five
will result in:
1. one
two
3. three
42. four
444. five
## Links
You can insert links inside your text in two ways:
some text [Inline-style](https://mlstate.com "MLstate") more text
or
some text [Reference-style][mlstate] some random text
[mlstate]: https://mlstate.com "MLstate"
In both cases, the title `("MLstate")` is optional. The result of the above is:
some text [Inline-style](https://mlstate.com "MLstate") more text
or
some text [Reference-style][mlstate] some random text
[mlstate]: https://mlstate.com "MLstate"
Note that references are case-sensitive and can be used for several links.
## Images
Image insertion uses the same syntax than inserting links preceded by a `!`:
![HTML5][html5]
[html5]: http://www.w3.org/html/logo/badge/html5-badge-h-solo.png "HTML5"
both result in:
![HTML5][html5]
[html5]: http://www.w3.org/html/logo/badge/html5-badge-h-solo.png "HTML5"
You can use the same reference for a link and an image (referencing the same URL).
## Code
There are two ways of inserting code inside your text.
Firstly, you can surround it with `\``, so `\`some code\`` will
result in `some code`.
You can also indent a paragraph with at least four spaces or a tabulation:
rec fact(x) =
if x < 1 then 1
else x * fact(x-1)
will result in:
rec fact(x) =
if x < 1 then 1
else x * fact(x-1)
## Quote
You can insert a quote in you texts by preceding it with `>`. You
can put a quote inside a quote:
> > An indented quote
> A standard quote
will result in:
> > An indented quote
> A standard quote
## Other
You can insert an html line break (`<br/>`) by putting two spaces at
the end of the line.
You can insert a horizontal line by writing a line containing only
the character `-` preceded by an empty line (otherwise it would result
in a second-level header).
--------------
Some text
with a linebreak
will result in:
--------------
Some text
with a linebreak
Comments