theorem
MeasRender_dom_monotonic
{α : Type}
{d : Doc}
{c : ℕ}
{i : ℕ}
{m₁ : Meas}
{c' : ℕ}
{i' : ℕ}
{m₂ : Meas}
{F : Factory α}
(h : MeasRender F d c i m₁)
(h' : MeasRender F d c' i' m₂)
(h_c : c ≤ c')
(h_i : i ≤ i')
:
Measure computation at higher column position or indentation level is worse
theorem
MeasRender_doc :
∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {m : Meas}, MeasRender F d c i m → Choiceless d → m.doc = d
Measure computation on a choiceless document preserves the doc component
theorem
MeasRender_dom_is_good
{α : Type}
{d : Doc}
{c : ℕ}
{i : ℕ}
{m₁ : Meas}
{c' : ℕ}
{i' : ℕ}
{m₂ : Meas}
{F : Factory α}
(h : MeasRender F d c i m₁)
(h' : MeasRender F d c' i' m₂)
(h_c : c ≤ c')
(h_i : i ≤ i')
(h_x : m₂.x ≤ F.W)
(h_y : m₂.y ≤ F.W)
:
If measure computation at higher column position or indentation level does not exceed the computation width limit, then the current measure computation also does not exceed the computation width limit