The Markdown container

def fence : List Char

```

def dd : List Char

$$

def dModel : List Char

::model[

def dRs : List Char

::reaction-system[

def dashes : List Char

---

def descInfo : List Char

The info string of the description block.

def dPlot : List Char

::plot{, the start of a plot directive.

def dRxn : List Char

$$\ce{, the start of a reaction line.

def dInit : List Char

The containers of initialization equations and constraints, and their end.

def dRole : Role → List Char

The opening line of the container of a role.

def dkw : DKind → List Char

The directive keyword of a declaration.

def dSub : List Char

::subsystem[, a subsystem included by reference.

def escKey (c : Char) : List Char

One character of a quoted key: the JSON escape, and the backtick as ``` (the info string of a backtick fence cannot hold a backtick).

def keyMd (k : String) : List Char

A path block’s key in the fence’s info string: bare when it is an identifier other than description (the description block), quoted otherwise.

def parseKeyMd (info : List Char) : Option String

Read a path block’s key from the info string (all of it).

def nameLatex (n : String) : List Char

A declared name, as LaTeX math under the empty symbol table (so it reads the same whatever else the document declares).

def pFlow : Nat → List Char → Option (Json × List Char)

A value: a flow collection at [ or {, else a scalar.

def pItemsF : Nat → List Char → Option (List Json × List Char)

The elements after the first, each after , , up to ].

def pEntryF : Nat → List Char → Option ((String × Json) × List Char)

One entry: key: value.

def pEntriesF : Nat → List Char → Option (List (String × Json) × List Char)

The entries after the first, each after , , up to }.

def isColl : Json → Bool

A value whose YAML starts with a bracket or brace (a list or an object, empty ones included): micromark-extension-directive, and so remark-directive, refuses such a value unquoted.

def sqEsc (cs : List Char) : List Char

The text of a single-quoted attribute value: ' as ' and & as &, the character references micromark-extension-directive decodes inside a quoted value.

def sqUnesc : List Char → List Char

Undo sqEsc .

def attrVal (v : Json) : List Char

An attribute value: a scalar as its YAML, a list or object as its YAML flow collection single-quoted (shape='["x", "y"]').

def attrMd (a : String × Json) : List Char

One attribute: key=value.

def attrsMd : List (String × Json) → List Char

The attributes, separated by spaces.

def declMd (d : Decl) : List Char

:var[$N$]{default=100 units="mol"}.

def pQuoted (u : List Char) : Option (Json × List Char)

A single-quoted value after its opening quote: the YAML inside, then the text after the closing quote.

def pAttr (s : List Char) : Option ((String × Json) × List Char)

One attribute.

def pAttrsMore : Nat → List Char → Option (List (String × Json) × List Char)

The attributes after the first, each after a space, up to the closing brace.

def pAttrs (f : Nat) : List Char → Option (List (String × Json) × List Char)

The attributes after the opening brace, up to the closing one.

def declBody (f : Nat) (k : DKind) : List Char → Option (RItem × List Char)

A declaration after its [.

def fenceItem (info body : List Char) : Option RItem

A fenced block’s construct, from its info string and body.

def labelOK (sl : List Char) : Bool

An equation label after the closing $$: nothing, or {#id}, with spaces around.

def fenceAt (f : Nat) (u : List Char) : Option (RItem × List Char)

A fenced block after ```esm:.

def paramsTxt : List String → List Char

The parameters of a template header, separated by , .

def tmRaw (t : Tm String) : List Char

The math text of a template or rule display (one line).

def pName (s : List Char) : Option (String × List Char)

One parameter: a name, up to the next , or ).

def pParams : Nat → List Char → Option (List String × List Char)

The parameters after (, up to ) \coloneqq .

def splitAt (sep : List Char) : List Char → Option (List Char × List Char)

Split at the first occurrence of sep.

def tmLex (raw : List Char) : Option (String × List String × Option (List Char) × List Char)

Read the math text of a display as a template or rule: its name, its parameters, its left-hand side (a rule’s) and its body, as text.

def mathAt (f : Nat) (u : List Char) : Option (RItem × List Char)

A display after its opening $$: a template or rule when its math reads as one, otherwise an equation (optionally labelled).

def tmContAt (f : Nat) (u : List Char) : Option (RItem × List Char)

A template or rule with other fields, after :::template{ or :::rule{: the attributes, the display, and the closing ::: line.

def dirAt (K : Kind) (u : List Char) : Option (RItem × List Char)

A component directive after its [.

def latexR : RSurf

The math surface of reaction sides: LaTeX under the empty symbol table.

def arrowL : List Char

The arrow with the rate over it, around the rate’s text (which ends at its $).

def rxnEnd : List Char

After the products: the end of the math and the start of the label.

def rxnBody (x : Rxn String) : List Char

The text of a reaction line after $$\ce{.

def rxnAt (f : Nat) (u : List Char) : Option (RItem × List Char)

A reaction line after its $$\ce{.

def subAt (f : Nat) (u : List Char) : Option (RItem × List Char)

A subsystem directive after its ::subsystem[.

def plotAt (f : Nat) (u : List Char) : Option (RItem × List Char)

A plot directive after its ::plot{.

def contBody (ro : Role) : Nat → List Char → Option (List RItem × List Char)

The displays of a container, up to its closing ::: line; blank lines between them are skipped.

def contOpen (s : List Char) : Bool

A container starts here.

def contAt (f : Nat) (s : List Char) : Option (List RItem × List Char)

A container, at its opening line.

def blockOpen (s : List Char) : Bool

A block construct starts here (at the start of a line).

def declOpen (s : List Char) : Bool

A declaration starts here.

def blockAt (f : Nat) (s : List Char) : Option (RItem × List Char)

Read the block construct that starts here.

def declAt (f : Nat) (s : List Char) : Option (RItem × List Char)

Read the declaration that starts here.

def tableOpen : List Char

| decl | name |, the start of a declarations table.

def trimCell (s : String) : String

A cell without its surrounding spaces.

def headerCells (s : List Char) : List String

The header cells of a table line: the line split at |, each cell trimmed.

def rateTable (s : List Char) : Bool

The start of a reaction table with a rate column: a line starting with | that has a cell rate. It is not a reaction notation (Notation.variants, rejected), and the lexer refuses it rather than skipping it as prose, which would drop its reactions.

def pCols : Nat → List Char → Option (List String × List Char)

The attribute columns of the header, up to its newline.

def pCell : List Char → Option (Option Json × List Char)

One cell: value |, or | when the attribute is absent.

def pCells : List String → List Char → Option (List (String × Json) × List Char)

The cells of a row, one per attribute column.

def kindOf (w : List Char) : Option DKind

The directive keyword of a row.

def pRow (cols : List String) : List Char → Option (Decl × List Char)

One row: | var | $N$ | and the cells, then a newline.

def pRows (cols : List String) : Nat → List Char → Option (List Decl × List Char)

The rows, as long as lines start with | .

def sepOK (l : List Char) : Bool

The separator row: only |, -, : and spaces.

def tableAt (f : Nat) (s : List Char) : Option (List RItem × List Char)

A declarations table, at its | decl | name |.

def afterRun (n : Nat) : List Char → Option (List Char)

The text after the first occurrence of n backticks.

def skipCode (s : List Char) : List Char

The text after the code span that starts here (at a backtick).

def lex : Nat → Bool → List Char → Option (List RItem)

The Markdown lexer: the constructs of a text, skipping prose one character at a time and code spans whole. bol: the text starts at the beginning of a line. A malformed construct is an error (none).

def FStop (rest : List Char) : Prop

What may follow an attribute value: ,, ], }, a space or |.

def attrOK (a : String × Json) : Bool

An attribute the Markdown attribute syntax can hold: an identifier key and a well-formed value.

def declOK (d : Decl) : Bool

A declaration the Markdown syntax can hold.

def mhchemOK (x : Rxn String) : Bool

What mhchem reads as written: no escaped brace \{ or \} anywhere inside \ce{…} (mhchem matches braces by character and fails on them).

def rxnOK (x : Rxn String) : Bool

A reaction the Markdown syntax can hold: sides the side syntax holds, a rate on one line without $, an id label, and attributes the attribute syntax holds.

def subMd (d : Decl) : List Char

::subsystem[Name]{ref="…"}, on a line of its own.

def subOK (d : Decl) : Bool

A subsystem directive the syntax can hold.

def itemMd : RItem → List Char

The text of a construct. A description is written verbatim in its fence; a path block’s value in YAML; a declaration inline (no newline of its own).

def eqnLabeled (raw : String) (label : List Char) : List Char

A display equation with an equation label after its closing $$ ( {#eq-x}).

inductive Seg where
  | item (it : RItem)
  | labeled (raw : String) (label : List Char)
  | prose (p : List Char)
  | code (body : List Char)

A piece of a Markdown document: a construct, a labelled equation, prose, or a code span (`…`, whatever its content).

def render (segs : List Seg) : List Char

The text of a document body.

def segItems : List Seg → List RItem

The constructs of a document body: prose dropped, labels dropped.

def isBlock : RItem → Bool

A construct that must start a line (all but declarations).

def itemOK : RItem → Bool

What each construct’s content must satisfy for its text to read back.

def Inert : Bool → List Char → List Char → Prop

Prose that the lexer skips: at no character does a construct start (a block construct only matters at the start of a line), and it holds no backtick (code spans are their own pieces, Seg.code). t is the text after the prose.

def Valid : Bool → List Seg → Prop

A document body whose constructs read back: each construct’s content is spellable, block constructs start a line, labels are labels, and prose is inert.

def dispTxt (raw : String) : List Char

A display followed by a blank line.

def colText (k : String) : List Char

A header column.

def cellText : Option Json → List Char

A cell.

def rowText (cols : List String) (d : Decl) : List Char

A row of the table.

def tableText (cols : List String) (ds : List Decl) : List Char

A declarations table over the attribute columns cols.

def TableOK (cols : List String) (d : Decl) : Prop

A declaration a table over cols holds: its name and attributes spellable, and its attributes exactly the columns it has a value in, in column order.