Theorems about the measure computation/rendering relation ($⇓_\mathbb{M}$) #
theorem
MeasRender_deterministic
{α : Type}
{d : Doc}
{c : ℕ}
{i : ℕ}
{F : Factory α}
{m₁ : Meas}
{m₂ : Meas}
(h₁ : MeasRender F d c i m₁)
(h₂ : MeasRender F d c i m₂)
:
m₁ = m₂
Determinism of the measure computation relation (Section 5.3)
theorem
MeasRender_single_correct
{α : Type}
{d : Doc}
{c : ℕ}
{i : ℕ}
{s : String}
(F : Factory α)
(h_render : Render d c i { fst := s, rst := [] })
:
∃ cost y, MeasRender F d c i { last := c + String.length s, cost := cost, doc := d, x := c + String.length s, y := y }
Correctness of the measure computation relation when it results in one line (first part of Theorem 5.3)
theorem
MeasRender_multi_correct
{α : Type}
{d : Doc}
{c : ℕ}
{i : ℕ}
{s : String}
{ss : List String}
(F : Factory α)
(h_render : Render d c i { fst := s, rst := ss })
(h_non_empty : ss ≠ [])
:
∃ cost y,
MeasRender F d c i
{ last := String.length (List.getLast ss h_non_empty), cost := cost, doc := d,
x := Layout.max_with_offset c { fst := s, rst := ss }, y := y }
Correctness of the measure computation relation when it results in multiple lines (second part of Theorem 5.3)
theorem
MeasRender_total
{α : Type}
(F : Factory α)
(d : Doc)
(c : ℕ)
(i : ℕ)
(h : Choiceless d)
:
∃ m, MeasRender F d c i m
Totality of the measure computation relation (Section 5.3)