diff --git a/.gitignore b/.gitignore index 1dee1865..0579592e 100644 --- a/.gitignore +++ b/.gitignore @@ -12,3 +12,6 @@ _out *.hash profile.json profile.json.gz +multi.json +single.json +*.html diff --git a/index.html b/index.html deleted file mode 100644 index becf8be7..00000000 --- a/index.html +++ /dev/null @@ -1,71 +0,0 @@ - - - An Astounding Document - - -
-

- An Astounding Document

-

- Today is 2029-04-01. This document was created on 2024-05-13.

-
-

- One Section

-

- Incoming links:

- -

- Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. At tellus at urna condimentum mattis pellentesque. Nisi vitae suscipit tellus mauris a diam. Nulla pharetra diam sit amet. Auctor neque vitae tempus quam pellentesque nec nam aliquam sem. Nibh venenatis cras sed felis eget velit aliquet sagittis id. A iaculis at erat pellentesque. Quis imperdiet massa tincidunt nunc pulvinar sapien et. Gravida dictum fusce ut placerat orci nulla pellentesque dignissim enim. Nulla facilisi etiam dignissim diam quis enim lobortis.

-

- Mauris nunc congue nisi vitae suscipit tellus. Facilisis gravida neque convallis a. Risus in hendrerit gravida rutrum. Tortor at risus viverra adipiscing at in. Velit laoreet id donec ultrices tincidunt arcu non. Ut lectus arcu bibendum at varius vel. Metus vulputate eu scelerisque felis. Id consectetur purus ut faucibus pulvinar elementum. Purus faucibus ornare suspendisse sed nisi lacus sed viverra tellus. Faucibus pulvinar elementum integer enim. Tincidunt arcu non sodales neque sodales ut. Est velit egestas dui id ornare arcu odio ut sem. Id aliquet lectus proin nibh nisl condimentum id venenatis. Sed vulputate mi sit amet mauris. Posuere ac ut consequat semper viverra nam libero justo. Mi quis hendrerit dolor magna eget est. Neque convallis a cras semper auctor neque. Quam adipiscing vitae proin sagittis nisl rhoncus mattis rhoncus. Leo vel fringilla est ullamcorper eget nulla facilisi etiam dignissim.

-

- Eleifend donec pretium vulputate sapien nec sagittis aliquam malesuada. In pellentesque massa placerat duis. Ac tortor vitae purus faucibus ornare suspendisse sed. Euismod lacinia at quis risus sed vulputate odio ut enim. Commodo viverra maecenas accumsan lacus. Phasellus egestas tellus rutrum tellus pellentesque eu tincidunt tortor. Nunc faucibus a pellentesque sit amet porttitor eget. Diam sit amet nisl suscipit adipiscing bibendum est. Morbi enim nunc faucibus a pellentesque sit amet. Amet commodo nulla facilisi nullam vehicula ipsum a arcu. Sodales ut eu sem integer vitae justo eget magna. Risus pretium quam vulputate dignissim suspendisse in. Malesuada fames ac turpis egestas integer eget aliquet nibh praesent. Quis varius quam quisque id diam. Ut consequat semper viverra nam libero justo. Adipiscing commodo elit at imperdiet dui accumsan sit. Sit amet facilisis magna etiam tempor orci. Faucibus pulvinar elementum integer enim neque volutpat. Sed sed risus pretium quam vulputate dignissim suspendisse in est. Nisi quis eleifend quam adipiscing vitae.

-

- Mi proin sed libero enim sed faucibus turpis. Nibh ipsum consequat nisl vel pretium. Ultricies lacus sed turpis tincidunt id aliquet risus. Est placerat in egestas erat imperdiet. Pretium vulputate sapien nec sagittis aliquam malesuada bibendum arcu. Turpis in eu mi bibendum neque egestas. Purus in massa tempor nec feugiat. In cursus turpis massa tincidunt dui. Consequat ac felis donec et odio pellentesque diam volutpat commodo. Fringilla ut morbi tincidunt augue. Pellentesque adipiscing commodo elit at imperdiet. Aliquam sem fringilla ut morbi tincidunt augue interdum velit euismod. Maecenas volutpat blandit aliquam etiam erat velit scelerisque in. Risus sed vulputate odio ut enim blandit volutpat. Nisi lacus sed viverra tellus. Nunc mi ipsum faucibus vitae aliquet nec ullamcorper. Consequat interdum varius sit amet mattis vulputate enim nulla aliquet.

-

- Eget mi proin sed libero enim. Nisl nunc mi ipsum faucibus vitae aliquet nec ullamcorper sit. Tincidunt arcu non sodales neque sodales ut etiam sit. Sed nisi lacus sed viverra tellus. Parturient montes nascetur ridiculus mus mauris vitae. Arcu cursus vitae congue mauris rhoncus. Est sit amet facilisis magna etiam tempor. Egestas diam in arcu cursus euismod quis. Sollicitudin tempor id eu nisl nunc mi. At auctor urna nunc id cursus metus aliquam. Ut sem viverra aliquet eget sit amet tellus cras adipiscing. Massa ultricies mi quis hendrerit dolor magna eget. Fermentum odio eu feugiat pretium nibh. Urna porttitor rhoncus dolor purus non. Egestas dui id ornare arcu. Massa id neque aliquam vestibulum morbi blandit.

-
-
-

- Another Section

-

- Incoming links:

- -

- Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. At tellus at urna condimentum mattis pellentesque. Nisi vitae suscipit tellus mauris a diam. Nulla pharetra diam sit amet. Auctor neque vitae tempus quam pellentesque nec nam aliquam sem. Nibh venenatis cras sed felis eget velit aliquet sagittis id. A iaculis at erat pellentesque. Quis imperdiet massa tincidunt nunc pulvinar sapien et. Gravida dictum fusce ut placerat orci nulla pellentesque dignissim enim. Nulla facilisi etiam dignissim diam quis enim lobortis.

-

- Mauris nunc congue nisi vitae suscipit tellus. Facilisis gravida neque convallis a. Risus in hendrerit gravida rutrum. Tortor at risus viverra adipiscing at in. Velit laoreet id donec ultrices tincidunt arcu non. Ut lectus arcu bibendum at varius vel. Metus vulputate eu scelerisque felis. Id consectetur purus ut faucibus pulvinar elementum. Purus faucibus ornare suspendisse sed nisi lacus sed viverra tellus. Faucibus pulvinar elementum integer enim. Tincidunt arcu non sodales neque sodales ut. Est velit egestas dui id ornare arcu odio ut sem. Id aliquet lectus proin nibh nisl condimentum id venenatis. Sed vulputate mi sit amet mauris. Posuere ac ut consequat semper viverra nam libero justo. Mi quis hendrerit dolor magna eget est. Neque convallis a cras semper auctor neque. Quam adipiscing vitae proin sagittis nisl rhoncus mattis rhoncus. Leo vel fringilla est ullamcorper eget nulla facilisi etiam dignissim.

-

- There are references to one section and another.

-

- Eleifend donec pretium vulputate sapien nec sagittis aliquam malesuada. In pellentesque massa placerat duis. Ac tortor vitae purus faucibus ornare suspendisse sed. Euismod lacinia at quis risus sed vulputate odio ut enim. Commodo viverra maecenas accumsan lacus. Phasellus egestas tellus rutrum tellus pellentesque eu tincidunt tortor. Nunc faucibus a pellentesque sit amet porttitor eget. Diam sit amet nisl suscipit adipiscing bibendum est. Morbi enim nunc faucibus a pellentesque sit amet. Amet commodo nulla facilisi nullam vehicula ipsum a arcu. Sodales ut eu sem integer vitae justo eget magna. Risus pretium quam vulputate dignissim suspendisse in. Malesuada fames ac turpis egestas integer eget aliquet nibh praesent. Quis varius quam quisque id diam. Ut consequat semper viverra nam libero justo. Adipiscing commodo elit at imperdiet dui accumsan sit. Sit amet facilisis magna etiam tempor orci. Faucibus pulvinar elementum integer enim neque volutpat. Sed sed risus pretium quam vulputate dignissim suspendisse in est. Nisi quis eleifend quam adipiscing vitae.

-

- Mi proin sed libero enim sed faucibus turpis. Nibh ipsum consequat nisl vel pretium. Ultricies lacus sed turpis tincidunt id aliquet risus. Est placerat in egestas erat imperdiet. Pretium vulputate sapien nec sagittis aliquam malesuada bibendum arcu. Turpis in eu mi bibendum neque egestas. Purus in massa tempor nec feugiat. In cursus turpis massa tincidunt dui. Consequat ac felis donec et odio pellentesque diam volutpat commodo. Fringilla ut morbi tincidunt augue. Pellentesque adipiscing commodo elit at imperdiet. Aliquam sem fringilla ut morbi tincidunt augue interdum velit euismod. Maecenas volutpat blandit aliquam etiam erat velit scelerisque in. Risus sed vulputate odio ut enim blandit volutpat. Nisi lacus sed viverra tellus. Nunc mi ipsum faucibus vitae aliquet nec ullamcorper. Consequat interdum varius sit amet mattis vulputate enim nulla aliquet.

-

- Eget mi proin sed libero enim. Nisl nunc mi ipsum faucibus vitae aliquet nec ullamcorper sit. Tincidunt arcu non sodales neque sodales ut etiam sit. Sed nisi lacus sed viverra tellus. Parturient montes nascetur ridiculus mus mauris vitae. Arcu cursus vitae congue mauris rhoncus. Est sit amet facilisis magna etiam tempor. Egestas diam in arcu cursus euismod quis. Sollicitudin tempor id eu nisl nunc mi. At auctor urna nunc id cursus metus aliquam. Ut sem viverra aliquet eget sit amet tellus cras adipiscing. Massa ultricies mi quis hendrerit dolor magna eget. Fermentum odio eu feugiat pretium nibh. Urna porttitor rhoncus dolor purus non. Egestas dui id ornare arcu. Massa id neque aliquam vestibulum morbi blandit.

-
-

- Some Subsection

-

- With a reference to the parent. -

-
-
-
- - - diff --git a/lean-toolchain b/lean-toolchain index 385b58a4..3b22be14 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-01-16 +leanprover/lean4:nightly-2026-01-20 diff --git a/multi.json b/multi.json deleted file mode 100644 index 59056a1e..00000000 --- a/multi.json +++ /dev/null @@ -1 +0,0 @@ -{"text":{"content":[{"concat":[{"other":{"container":{"data":null,"id":1,"name":"Verso.Genre.Manual.Block.paragraph","properties":{}},"content":[{"para":[{"text":"Verso is a tool for writing about Lean."},{"linebreak":"\n"},{"text":"Or, rather, it is a framework for constructing such tools, together with concrete tools that use this framework."},{"linebreak":"\n"},{"text":"Technical writing can take many forms, including but not limited to:"}]},{"ul":[{"contents":[{"para":[{"text":"Reference manuals"}]}]},{"contents":[{"para":[{"text":"Tutorials"}]}]},{"contents":[{"para":[{"text":"Web pages"}]}]},{"contents":[{"para":[{"text":"Academic papers"}]}]}]}]}}]},{"para":[{"text":"All of these genres have common concerns, such as displaying Lean code, including tests to prevent bit-rot of the text, and linking to other resources."},{"linebreak":"\n"},{"text":"However, they are also very different."},{"linebreak":"\n"},{"text":"Some have a very linear structure, while others combine date-based content with an unordered set of pages."},{"linebreak":"\n"},{"text":"Some should generate highly interactive output, while others should generate PDFs that can be turned into published papers books."}]},{"para":[{"text":"Verso consists of the following components:"}]},{"dl":[{"contents":[{"para":[{"text":"Verso's "},{"other":{"container":{"data":{"canonicalName":"verso-markup","domain":"Verso.Genre.Manual.section","remote":null,"resolvedDestination":"/Verso-Markup/#verso-markup"},"id":618,"name":"Verso.Genre.Manual.Inline.ref"},"content":[{"text":"markup language"}]}},{"text":" is a simplified variant of Markdown."},{"linebreak":"\n"},{"text":" It is also an alternative concrete syntax for Lean itself, so Verso documents are just Lean files."},{"linebreak":"\n"},{"text":" Just as TeX, Sphinx, and Scribble allow their languages to be extended using their own programming languages, Verso's markup language is extensible."},{"linebreak":"\n"},{"text":" Define a Lean function at the top of a file, and use it in the text of that very same file."}]}],"term":[{"text":" Markup language"}]},{"contents":[{"para":[{"text":"All Verso documents can contain a set of "},{"other":{"container":{"data":{"canonicalName":"elaboration","domain":"Verso.Genre.Manual.section","remote":null,"resolvedDestination":"/Building-Documents/Elaboration/#elaboration"},"id":619,"name":"Verso.Genre.Manual.Inline.ref"},"content":[{"text":"common elements"}]}},{"text":", such as paragraphs, emphasized text, or images."},{"linebreak":"\n"},{"text":" They also share a hierarchical structure of sections and subsections."},{"linebreak":"\n"},{"text":" These types are extensible by individual genres."}]}],"term":[{"text":" Extensible document structure"}]},{"contents":[{"para":[{"text":"Verso provides a shared paradigm for converting text written by an author into readable output."},{"linebreak":"\n"},{"text":" Different genres will produce different output formats, but they don't need to reinvent the wheel in order to resolve cross-references, and they can benefit from shared libraries for producing output in various formats."}]}],"term":[{"text":" Elaboration and rendering framework"}]},{"contents":[{"para":[{"text":"Verso includes a common paradigm for representing the documented items, and a format for sharing cross-reference databases between genres that emit HTML, which enables links and cross-references to be automatically inserted and maintained."}]}],"term":[{"text":" Cross-reference management"}]},{"contents":[{"para":[{"text":"Verso includes facilities for elaborating and displaying Lean code in documents."},{"linebreak":"\n"},{"text":" In HTML output, this code is rendered with toggleable proof states, hovers, and hyperlinks."},{"linebreak":"\n"},{"text":" It's also highlighted accurately, which is impossible with regexp-based highlighting due to Lean's syntactic extensibility."}]},{"para":[{"text":"The "},{"link":{"content":[{"code":"SubVerso"}],"url":"https://github.com/leanprover/subverso"}},{"text":" helper library allows Verso documents to process Lean code written in any version of Lean, starting with "},{"code":"4.0.0"},{"text":"."},{"linebreak":"\n"},{"text":" This makes it possible to write a document that compares and contrasts versions, or to decouple upgrades to the Lean version used in a project from the Lean version used in the document that describes it."}]}],"term":[{"text":" Lean rendering"}]},{"contents":[{"para":[{"text":"Verso includes utility libraries that can be used by genres to provide features such as full-text search of HTML content."},{"linebreak":"\n"},{"text":" These libraries have no additional build-time dependencies, avoiding the complications of staying up to date with multiple library ecosystems at once."}]}],"term":[{"text":" Utility libraries"}]}]}],"metadata":{"assignedNumber":null,"authors":["David Thrane Christiansen"],"authorshipNote":null,"date":null,"draft":false,"file":null,"htmlSplit":"default","htmlToc":true,"id":0,"number":true,"shortContextTitle":null,"shortTitle":"Documentation with Verso","tag":{"external":{"name":"Writing-Documentation-in-Lean-with-Verso"}}},"subParts":[{"content":[{"concat":[{"other":{"container":{"data":null,"id":5,"name":"Verso.Genre.Manual.Block.paragraph","properties":{}},"content":[{"para":[{"text":"Documentation comes in many forms, and no one system is suitable for representing all of them."},{"linebreak":"\n"},{"text":"The needs of software documentation writers are not the same as the needs of textbook authors, researchers writing papers, bloggers, or poets."},{"linebreak":"\n"},{"text":"Thus, Verso supports multiple "},{"other":{"container":{"data":["genre","genres"],"id":6,"name":"Verso.Genre.Manual.deftech"},"content":[{"emph":[{"text":"genres"}]}]}},{"text":", each of which consists of:"}]},{"ul":[{"contents":[{"para":[{"text":"A global view of a document's structure, whether it be a document with subsections, a collection of interrelated documents such as a web site, or a single file of text"}]}]},{"contents":[{"para":[{"text":"A representation of cross-cutting state such as cross-references to figures, index entries, and named theorems"}]}]},{"contents":[{"para":[{"text":"Additions to the structure of the document - for instance, the blog genre supports the inclusion of raw HTML, and the manual genre supports grouping multiple top-level blocks into a single logical paragraph"}]}]},{"contents":[{"para":[{"text":"Procedures for resolving cross references and rendering the document to one or more output formats"}]}]}]},{"para":[{"text":"All genres use the same "},{"other":{"container":{"data":{"canonicalName":"verso-markup","domain":"Verso.Genre.Manual.section","remote":null,"resolvedDestination":"/Verso-Markup/#verso-markup"},"id":620,"name":"Verso.Genre.Manual.Inline.ref"},"content":[{"text":"markup syntax"}]}},{"text":", and they can share extensions to the markup language that don't rely on incompatible document structure additions."},{"linebreak":"\n"},{"text":"Mixing incompatible features results in an ordinary Lean type error."}]}]}}]}],"metadata":{"assignedNumber":1,"authors":[],"authorshipNote":null,"date":null,"draft":false,"file":null,"htmlSplit":"default","htmlToc":true,"id":4,"number":true,"shortContextTitle":null,"shortTitle":null,"tag":{"external":{"name":"genres"}}},"subParts":[],"title":[{"text":"Genres"}],"titleString":"Genres"},{"content":[{"para":[{"text":"Lean's documentation markup language is a close relative of Markdown, but it's not identical to it."}]}],"metadata":{"assignedNumber":2,"authors":[],"authorshipNote":null,"date":null,"draft":false,"file":null,"htmlSplit":"never","htmlToc":true,"id":8,"number":true,"shortContextTitle":null,"shortTitle":null,"tag":{"external":{"name":"verso-markup"}}},"subParts":[{"content":[{"dl":[{"contents":[{"para":[{"text":"Fail fast rather than producing unexpected output or having complicated rules."}]}],"term":[{"text":" Syntax errors"}]},{"contents":[{"para":[{"text":"Parsing should succeed or fail as locally as possible."}]}],"term":[{"text":" Reduce lookahead"}]},{"contents":[{"para":[{"text":"There should be dedicated features for compositionally adding new kinds of content, rather than relying on a collection of ad-hoc textual subformats."}]}],"term":[{"text":" Extensibility"}]},{"contents":[{"para":[{"text":"Lean users are used to entering Unicode directly and have good tools for it, so there's no need to support alternative textual syntaxes for characters not on keyboards such as em dashes or typographical quotes."}]}],"term":[{"text":" Assume Unicode"}]},{"contents":[{"para":[{"text":"Users benefit from existing muscle memory and familiarity when it doesn't lead to violations of the other principles."}]}],"term":[{"text":" Markdown compatibility"}]}]}],"metadata":{"assignedNumber":1,"authors":[],"authorshipNote":null,"date":null,"draft":false,"file":null,"htmlSplit":"default","htmlToc":true,"id":9,"number":true,"shortContextTitle":null,"shortTitle":null,"tag":{"external":{"name":"markup-design-principles"}}},"subParts":[],"title":[{"text":"Design Principles"}],"titleString":"Design Principles"},{"content":[{"para":[{"text":"Like Markdown, Lean's markup has three primary syntactic categories:"}]},{"dl":[{"contents":[{"para":[{"text":"Headers, footnote definitions, and named links give greater structure to a document. They may not be nested inside of blocks."}]}],"term":[{"text":" Document structure"}]},{"contents":[{"para":[{"text":"The main organization of written text, including paragraphs, lists, and quotations. Some blocks may be nested: for example, lists may contain other lists."}]}],"term":[{"text":" Block elements"}]},{"contents":[{"para":[{"text":"The ordinary content of written text, such as text itself, bold or emphasized text, and hyperlinks."}]}],"term":[{"text":" Inline elements"}]}]}],"metadata":{"assignedNumber":2,"authors":[],"authorshipNote":null,"date":null,"draft":false,"file":null,"htmlSplit":"default","htmlToc":true,"id":10,"number":true,"shortContextTitle":null,"shortTitle":null,"tag":{"external":{"name":"markup-syntax"}}},"subParts":[{"content":[{"para":[{"text":"Documents are organized into "},{"other":{"container":{"data":["part","parts"],"id":12,"name":"Verso.Genre.Manual.deftech"},"content":[{"emph":[{"text":"parts"}]}]}},{"text":"."},{"linebreak":"\n"},{"text":"A part is a logical division of the content of the document, such as a chapter, section, subsection, or volume."},{"linebreak":"\n"},{"text":"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 "},{"other":{"container":{"data":["genre","/home/runner/work/verso/verso/doc/UsersGuide/Markup.lean:401:210",null],"id":13,"name":"Verso.Genre.Manual.tech"},"content":[{"text":"genre"}]}},{"text":"."}]},{"para":[{"text":"A part contains a sequence of blocks followed by a sequence of sub-parts, either of which may be empty."}]},{"para":[{"text":"A part is introduced with a "},{"other":{"container":{"data":["header","header"],"id":14,"name":"Verso.Genre.Manual.deftech"},"content":[{"emph":[{"text":"header"}]}]}},{"text":"."},{"linebreak":"\n"},{"text":"Headers consist of one or more hash marks ("},{"code":"#"},{"text":") at the beginning of a line followed by a sequence of inlines."},{"linebreak":"\n"},{"text":"The number of hash marks indicates the nesting of a header, and headers with more hash marks indicate parts at a lower level."},{"linebreak":"\n"},{"text":"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."},{"linebreak":"\n"},{"text":"In other words, header levels induce a tree structure on the document."}]},{"para":[{"text":"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."},{"linebreak":"\n"},{"text":"This is a "},{"emph":[{"text":"syntactic"}]},{"text":" 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."},{"linebreak":"\n"},{"text":"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."}]},{"para":[{"text":"Metadata may be associated with a header by following it with a "},{"other":{"container":{"data":["metadata block","metadata block"],"id":15,"name":"Verso.Genre.Manual.deftech"},"content":[{"emph":[{"text":"metadata block"}]}]}},{"text":"."},{"linebreak":"\n"},{"text":"Metadata blocks begin and end with "},{"code":"%%%"},{"text":", and they contain any syntax that would be acceptable in a Lean structure initializer."}]},{"concat":[{"other":{"container":{"data":"Header","id":16,"name":"MarkupExample","properties":{}},"content":[{"code":"# Top-Level Header\n"},{"code":"

Top-Level Header

\n"}]}}]},{"concat":[{"other":{"container":{"data":"Blah","id":17,"name":"MarkupExample","properties":{}},"content":[{"code":"a b c\n"},{"code":"

a b c

"}]}}]}],"metadata":{"assignedNumber":1,"authors":[],"authorshipNote":null,"date":null,"draft":false,"file":null,"htmlSplit":"default","htmlToc":true,"id":11,"number":true,"shortContextTitle":null,"shortTitle":null,"tag":{"external":{"name":"document-structure"}}},"subParts":[],"title":[{"text":"Document Structure"}],"titleString":"Document Structure"},{"content":[{"para":[{"text":"Paragraphs are undecorated: any sequence of inlines that is not another block is a paragraph."},{"linebreak":"\n"},{"text":"Paragraphs continue until a "},{"other":{"container":{"data":["blank line","blank line"],"id":19,"name":"Verso.Genre.Manual.deftech"},"content":[{"emph":[{"text":"blank line"}]}]}},{"text":" (that is, a line containing only whitespace) or another block begins:"}]},{"concat":[{"other":{"container":{"data":"Paragraphs","id":20,"name":"MarkupExample","properties":{}},"content":[{"code":"This is one paragraph.\nEven though this sentence is on a\nnew line, the paragraph continues.\n\nThis is a new paragraph.\n* This list stopped the paragraph.\n* As in Markdown and SGML, lists\n are not part of paragraphs.\n"},{"code":"

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

\n\n

This is a new paragraph.

\n\n"}]}}]}],"metadata":{"assignedNumber":2,"authors":[],"authorshipNote":null,"date":null,"draft":false,"file":null,"htmlSplit":"default","htmlToc":true,"id":18,"number":true,"shortContextTitle":null,"shortTitle":null,"tag":{"external":{"name":"block-syntax"}}},"subParts":[{"content":[{"para":[{"text":"There are three kinds of lists:"}]},{"dl":[{"contents":[{"para":[{"text":"Unordered lists indicate that the order of the items in the list is not of primary importance."},{"linebreak":"\n"},{"text":" They correspond to "},{"code":"