ink

inductive Resolve {α : Type} (F : Factory α) : Doc → ℕ → ℕ → MeasureSet → Prop

• line_taint: ∀ {α : Type} {F : Factory α} {c i : ℕ} {m : Meas}, c > F.W ∨ i > F.W → MeasRender F Doc.nl c i m → Resolve F Doc.nl c i (MeasureSet.tainted m)
• line_set: ∀ {α : Type} {F : Factory α} {c i : ℕ} {m : Meas}, c ≤ F.W → i ≤ F.W → MeasRender F Doc.nl c i m → Resolve F Doc.nl c i (MeasureSet.set [m] (_ : ¬[m] = []))
• text_taint: ∀ {α : Type} {F : Factory α} {c i : ℕ} {s : String} {m : Meas}, c + String.length s > F.W ∨ i > F.W → MeasRender F (Doc.text s) c i m → Resolve F (Doc.text s) c i (MeasureSet.tainted m)
• text_set: ∀ {α : Type} {F : Factory α} {c i : ℕ} {s : String} {m : Meas}, c + String.length s ≤ F.W → i ≤ F.W → MeasRender F (Doc.text s) c i m → Resolve F (Doc.text s) c i (MeasureSet.set [m] (_ : ¬[m] = []))
• align_taint: ∀ {α : Type} {F : Factory α} {i : ℕ} {d : Doc} {c : ℕ} {ms : MeasureSet}, i > F.W → Resolve F d c c ms → Resolve F (Doc.align d) c i (MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms))
• align: ∀ {α : Type} {F : Factory α} {i : ℕ} {d : Doc} {c : ℕ} {ms : MeasureSet}, i ≤ F.W → Resolve F d c c ms → Resolve F (Doc.align d) c i (MeasureSet.lift (Meas.adjust_align i) ms)
• nest: ∀ {α : Type} {F : Factory α} {d : Doc} {c i n : ℕ} {ms : MeasureSet}, Resolve F d c (i + n) ms → Resolve F (Doc.nest n d) c i (MeasureSet.lift (Meas.adjust_nest n) ms)
• choice: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms : MeasureSet} {d' : Doc} {ms' : MeasureSet}, Resolve F d c i ms → Resolve F d' c i ms' → Resolve F (Doc.choice d d') c i (MeasureSet.union F ms ms')
• concat_taint: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {m : Meas} {d' : Doc} {ms' : MeasureSet} {m' : Meas}, Resolve F d c i (MeasureSet.tainted m) → Resolve F d' m.last i ms' → MeasureSet.taint ms' = MeasureSet.tainted m' → Resolve F (Doc.concat d d') c i (MeasureSet.tainted (Meas.concat F m m'))
• concat_set: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms : List Meas} {h_non_empty : ms ≠ []} {d' : Doc} {msr : MeasureSet}, Resolve F d c i (MeasureSet.set ms h_non_empty) → ResolveConcat F ms d' i msr → Resolve F (Doc.concat d d') c i msr

ink

inductive ResolveConcat {α : Type} (F : Factory α) : List Meas → Doc → ℕ → MeasureSet → Prop

• one: ∀ {α : Type} {F : Factory α} {d : Doc} {m : Meas} {i : ℕ} {msr : MeasureSet}, ResolveConcatOne F d m i msr → ResolveConcat F [m] d i msr
• cons: ∀ {α : Type} {F : Factory α} {ms : List Meas} {d : Doc} {i : ℕ} {msr : MeasureSet} {m : Meas} {msr' : MeasureSet}, ResolveConcat F ms d i msr → ResolveConcatOne F d m i msr' → ResolveConcat F (m :: ms) d i (MeasureSet.union F msr' msr)

ink

inductive ResolveConcatOne {α : Type} (F : Factory α) : Doc → Meas → ℕ → MeasureSet → Prop

• tainted: ∀ {α : Type} {F : Factory α} {d : Doc} {i : ℕ} {m' m : Meas}, Resolve F d m.last i (MeasureSet.tainted m') → ResolveConcatOne F d m i (MeasureSet.tainted (Meas.concat F m m'))
• set: ∀ {α : Type} {F : Factory α} {d : Doc} {i : ℕ} {ms : List Meas} {h_non_empty : ms ≠ []} {m : Meas}, Resolve F d m.last i (MeasureSet.set ms h_non_empty) → ResolveConcatOne F d m i (MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms)) (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms) ≠ []))