Theorems about the rendering relation ($⇓_\mathcal{R}$)

ink

theorem Render_deterministic {d : Doc} {c : ℕ} {i : ℕ} {L₁ : Layout} {L₂ : Layout} (h₁ : Render d c i L₁) (h₂ : Render d c i L₂) : L₁ = L₂

Determinism of the rendering relation (Section 3.3)

ink

theorem Render_total {d : Doc} (c : ℕ) (i : ℕ) (h : Choiceless d) : ∃ L, Render d c i L

Totality of the rendering relation (Section 3.3)