Line heads of the YAML spelling

Lean module Esm.Document.Source.YamlLines, formal/Esm/Document/Source/YamlLines.lean at 184aa13d35e5
Imports Esm.Document.Yaml, Esm.Document.Source.Lines

Facts about which characters start a line of Yaml.encode v, used to show a YAML block can sit inside a Markdown code fence (yaml_heads_tick ) or between front-matter --- delimiters (yaml_heads_dash ), and that it ends at the start of a line (yaml_ends ).

No raw newlines in scalars and keys

Line heads

def HeadsP source

def HeadsP (p : Char → Prop) (l : List Char) : Prop

Every character that starts a line of l, wherever l starts, satisfies p.

theorem HeadsP.cons_mid proved source

theorem HeadsP.cons_mid {p : Char → Prop} {x : Char} {r : List Char} (hx : p x) (hn : x ≠ '\n')
    (hr : ∀ c ∈ heads false r, p c) : HeadsP p (x :: r)

A first character that is not a newline: what follows is read mid-line.

theorem HeadsP.line proved source

theorem HeadsP.line {p : Char → Prop} {x : Char} (hx : p x) (hxn : x ≠ '\n') (hn : p '\n')
    {t : List Char} (ht : '\n' ∉ t) : HeadsP p (x :: (t ++ ['\n']))

One line x :: t ending in a newline.

theorem HeadsP.scalarLine proved source

theorem HeadsP.scalarLine {p : Char → Prop} (hs : p ' ') (hn : p '\n') {x : List Char}
    (hx : '\n' ∉ x) : HeadsP p (' ' :: (x ++ ['\n']))

A line x ending in a newline, where x has no newline.

abbrev Good source

abbrev Good (c : Char) : Prop

Not a backtick and not a dash.

theorem items_good proved source

theorem items_good (m : Nat) : ∀ l : List Json, HeadsP Good (encItems (m + 1) l)

At a positive indentation every item line starts with a space.

theorem items_tick proved source

theorem items_tick : ∀ l : List Json, HeadsP (· ≠ '`') (encItems 0 l)

At indentation 0 an item line starts with -, never a backtick.

theorem inline_head proved source

theorem inline_head (v : Json) (hv : v.WF) (hi : isInl v = true) :
    ∃ c t, Yaml.inline v = c :: t ∧ c ≠ '`' ∧ c ≠ '\n'

A scalar or empty container starts with a character that is neither a backtick nor a newline. (A number needs WF: an out-of-range digit could print as a backtick.)

Line ends

The YAML spelling

theorem yaml_heads_tick proved source

theorem yaml_heads_tick (v : Json) (hv : v.WF) : '`' ∉ heads true (Yaml.encode v)

No line of the YAML spelling of a well-formed value starts with a backtick, so a YAML block never closes a Markdown code fence.

theorem yaml_heads_dash proved source

theorem yaml_heads_dash (kvs : List (String × Json)) (hv : (Json.obj kvs).WF) :
    '-' ∉ heads true (Yaml.encode (.obj kvs))

No line of the YAML spelling of a well-formed object starts with -, so front matter never contains the --- delimiter line.

theorem yaml_ends proved source

theorem yaml_ends (v : Json) : endBol false (Yaml.encode v) = true

The YAML spelling ends with a newline.

This module also proves 31 lemmas without doc comments; they are in the source.