2.2.1. Document Structure🔗

Documents are organized into parts. A part is a logical division of the content of the document, such as a chapter, section, subsection, or volume. Parts may have associated metadata, such as authors, publication dates, internal identifiers for cross-referencing, or desired URLs; the specific metadata associated with a part is determined by the document's genre.

A part contains a sequence of blocks followed by a sequence of sub-parts, either of which may be empty.

A part is introduced with a header. Headers consist of one or more hash marks (#) at the beginning of a line followed by a sequence of inlines. The number of hash marks indicates the nesting of a header, and headers with more hash marks indicate parts at a lower level. A lower-level header introduces a sub-part of the preceding header, while a header at a level at least as high as the preceding header terminates that part. In other words, header levels induce a tree structure on the document.

Headers must be well-nested: the first header in a document must have exactly one hash mark, and all subsequent headers may have at most one more hash mark than the preceding header. This is a syntactic requirement: regardless of whether a Verso file contains the text of a whole book, a chapter, or just a single section, its outermost header must be introduced with a single hash mark. Headers indicate the logical nesting structure of the document, rather than the headers to be chosen when rendering the document to output formats such as HTML.

Metadata may be associated with a header by following it with a metadata block. Metadata blocks begin and end with %%%, and they contain any syntax that would be acceptable in a Lean structure initializer.

# Top-Level Header

<h1>Top-Level Header</h1>

a b c

<p> a b c </p>

2.2.2. Block Syntax🔗

Paragraphs are undecorated: any sequence of inlines that is not another block is a paragraph. Paragraphs continue until a blank line (that is, a line containing only whitespace) or another block begins:

This is one paragraph.
Even though this sentence is on a
new line, the paragraph continues.

This is a new paragraph.
* This list stopped the paragraph.
* As in Markdown and SGML, lists
  are not part of paragraphs.

<p>
  This is one paragraph. Even
  though this sentence is on a new
  line, the paragraph continues.
</p>

<p> This is a new paragraph. </p>

<ul>
  <li>
    <p>
      This list stopped the
      paragraph.
    </p>
  </li>
  <li>
    <p>
      As in Markdown and SGML,
      lists   are not part of
      paragraphs.
    </p>
  </li>
</ul>

* A list with two items
* They both start in column 0

<ul>
  <li>
    <p> A list with two items </p>
  </li>
  <li>
    <p>
      They both start in column 0
    </p>
  </li>
</ul>

 * A list with two items
 * They both start in column 1

<ul>
  <li>
    <p> A list with two items </p>
  </li>
  <li>
    <p>
      They both start in column 1
    </p>
  </li>
</ul>

 * Two lists
 + They have different indicators.

<ul>
  <li> <p> Two lists </p> </li>
</ul>

<ul>
  <li>
    <p>
      They have different
      indicators.
    </p>
  </li>
</ul>

 * A list with one element
* Another list, due to different
  indentation

<ul>
  <li>
    <p>
      A list with one element
    </p>
  </li>
</ul>

<ul>
  <li>
    <p>
      Another list, due to
      different   indentation
    </p>
  </li>
</ul>

* A list with one item.
  It contains this paragraph

  * And this other sub-list

  And this paragraph

<ul>
  <li>
    <p>
      A list with one item.   It
      contains this paragraph
    </p><ul>
      <li>
        <p>
          And this other sub-list
        </p>
      </li>
    </ul><p>
      And this paragraph
    </p>
  </li>
</ul>

1. First, write a number.
2. Then, an indicator (`.` or `)`)

<ol>
  <li>
    <p> First, write a number. </p>
  </li>
  <li>
    <p>
      Then, an indicator
      (<code>"."</code> or
      <code>")"</code>)
    </p>
  </li>
</ol>

1. Two lists
2) They have different indicators.

<ol>
  <li> <p> Two lists </p> </li>
</ol>

<ol>
  <li>
    <p>
      They have different
      indicators.
    </p>
  </li>
</ol>

: Item 1

  Description of item 1

: Item 2

  Description of item 2

<dl>
    <dt>  Item 1 </dt>
  <dd>
    <p> Description of item 1 </p>
  </dd>
  
    <dt>  Item 2 </dt>
  <dd>
    <p> Description of item 2 </p>
  </dd>
   </dl>

It is said that:
> Quotations are excellent.

  This paragraph is part of the
  quotation.

 So is this one.

But not this one.

<p> It is said that: </p>

<blockquote>
  <p>
    Quotations are excellent.
  </p>
  <p>
    This paragraph is part of the  
    quotation.
  </p>
  <p> So is this one. </p>
</blockquote>

<p> But not this one. </p>

```
This is a code block
with two lines
```

<codeblock>
  1|This is a code block⏎
  2|with two lines⏎
</codeblock>

```lean
-- This code block is named
-- `lean`. It was called with
-- no arguments.
def x := 5
```

<lean >
  1|-- This code block is named⏎
  2|-- `lean`. It was called with⏎
  3|-- no arguments.⏎
  4|def x := 5⏎
</lean>

  ```lean
  -- This indented code block
  -- denotes the de-indented
  -- string
  def x := 5
  ```

<lean >
  1|-- This indented code block⏎
  2|-- denotes the de-indented⏎
  3|-- string⏎
  4|def x := 5⏎
</lean>

```lean (error := true)
-- This code block is named
-- `lean`, called with the
-- named argument `error`
-- set to `true`.
def x : String := 5
```

<lean  error="true">
  1|-- This code block is named⏎
  2|-- `lean`, called with the⏎
  3|-- named argument `error`⏎
  4|-- set to `true`.⏎
  5|def x : String := 5⏎
</lean>

:::nothing
:::

<nothing >  </nothing>

::::outer
:::inner
Hello
:::
This is a paragraph
::::

<outer >
  <inner > <p> Hello </p> </inner>
  <p> This is a paragraph </p>
</outer>

{include 0 MyChapter}

<include  0 MyChapter/>

2.2.3. Inline Syntax🔗

Emphasis is written with underscores:

Here's some _emphasized_ text

<p>
  Here's some
  <emph> emphasized </emph> text
</p>

Emphasis can be nested by using more underscores for the outer emphasis:

Here's some __emphasized text
with _extra_ emphasis__ inside

<p>
  Here's some
  <emph>
    emphasized text with
    <emph> extra </emph> emphasis
  </emph>
  inside
</p>

Strong emphasis (bold) is written with asterisks:

Here's some *bold* text

<p>
  Here's some <bold>bold</bold>
  text
</p>

Hyperlinks consist of the link text in square brackets followed by the target in parentheses:

[Lean](https://lean-lang.org)

<p>
  <a href="https://lean-lang.org">
    Lean
  </a>
</p>

Link targets may also be named:

The [Lean website][lean]

[lean]: https://lean-lang.org

<p>
  The
  <a href="(value of «lean»)">Lean
  website</a>
</p>

where
  «lean» := https://lean-lang.org

Literal code elements are written in back-ticks. The same number of back-ticks that opens a code element must be used to close it, and the code element may not contain a sequence of back-ticks that's at least as long as its opener and closer.

The definition of `main`

<p>
  The definition of
  <code>"main"</code>
</p>

As a special case, code inlines that being and end with a space denote the string that results from removing one leading and trailing space. This makes it possible to represent values that begin or end with back-ticks:

`` `quotedName ``

<p> <code>"`quotedName"</code> </p>

or with spaces:

``  one space  ``

<p> <code>" one space "</code> </p>

![Alt text](image.png)

<p>
  <img
    src="image.png"
    alt="Alt text"/>
</p>

![Alternative text][image]

[image]: image.png

<p>
  <img
    src="value of «image»"
    alt="Alternative text"/>
</p>

where «image» := image.png

TeX math can be included using a single or double dollar sign followed by code. Two dollar signs results in display-mode math, so $`\sum_{i=0}^{10} i` results in \sum_{i=0}^{10} i while $$`\sum_{i=0}^{10} i` results in: \sum_{i=0}^{10} i

A role indicates that subsequent inlines have a special meaning. Roles can be used to trigger special handling of code (e.g. elaboration), register definitions and uses of technical terms, add marginal notes, and much more. They correspond to custom commands in LaTeX. A role consists of curly braces that contain a name and arguments, all on the same line, followed immediately either by a self-delimiting inline or by square brackets that contain zero or more inlines.

An inline is self-delimiting if it has distinct start and end tokens that make its ending position clear. Emphasis, strong emphasis, code, links, images, math, and roles are self-delimiting.

{ref "chapter-tag"}[the chapter on
$`\frac{1}{2}`-powered syntax]

<p>
  <ref "chapter-tag">
    the chapter on  
    <math contents="\\frac{1}{2}"/>
    -powered syntax
  </ref>
</p>

{lean}`2 + f 4`

<p>
  <lean >
    <code>"2 + f 4"</code>
  </lean>
</p>

2.3.1. Syntax Errors🔗

While Markdown includes a set of precedence rules to govern the meaning of mismatched delimiters (such as in what _is *bold_ or emph*?), these are syntax errors in Lean's markup. Similarly, Markdown specifies that unmatched delimiters (such as * or _) should be included as characters, while Lean's markup requires explicit escaping of delimiters.

This is based on the principle that, for long-form technical writing, it's better to catch typos while writing than while reviewing the text later.

2.3.2. Reduced Lookahead🔗

In Markdown, whether [this][here] is a link depends on whether here is defined as a link reference target somewhere in the document. In Lean's markup, it is always a link, and it is an error if here is not defined as a link target.

2.3.3. Header Nesting🔗

In Lean's markup, every document already has a title, so there's no need to use the highest level header (#) to specify one. Additionally, all documents are required to use # for their top-level header, ## for the next level, and so forth, because a single file may represent a section, a chapter, or even a whole book. Authors should not need to maintain a global mapping from header levels to document structures, so Lean's markup automatically assigns these based on the structure of the document.

2.3.4. Genre-Specific Extensions🔗

Markdown has no standard way for specific tools or styles of writing to express domain- or genre-specific concepts. Lean's markup provides standard syntaxes to use for this purpose, enabling compositional extensions.

2.3.5. Fewer Unused Features🔗

Markdown has a number of features that are rarely used in practice. They have been removed from Verso to reduce surprises while using it and make documents more predictable. This includes:

• the distinction between tight and loose lists,

• four-space indentation to create code blocks,

• Setext-style headers, indicated with underlines instead of leading hash marks (#),

• hard line break syntax,

• and HTML entities and character references

Other Markdown features don't make sense for non-HTML output, and can be implemented by a genre using code blocks or directives. They have also been removed from Verso. In particular, this includes HTML blocks, raw HTML and thematic breaks.

Finally, some Markdown features are used by a minority of authors, and make sense in all backends, but were not deemed worth the complexity budget. In particular, this includes auto-links.