Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
import Pretty.Defs.Basic
import Pretty.Defs.MeasureSetOp
import Pretty.Supports.Dedup
section Resolve
variable ( F : Factory α )
mutual
inductive Resolve : Doc → ℕ → ℕ → @ MeasureSet α → Prop where
| line_taint ( h_bad : c > F . W ∨ i > F . W ) ( h : MeasRender F Doc.nl c i m ) :
Resolve Doc.nl c i ( MeasureSet.tainted : {α : Type } → Meas → MeasureSet m )
| line_set ( h_c : c ≤ F . W ) ( h_i : i ≤ F . W ) ( h : MeasRender F Doc.nl c i m ) :
Resolve Doc.nl c i ( MeasureSet.set : {α : Type } → (ms : List Meas ms ≠ [] MeasureSet [ m ] ( by simp ))
| text_taint ( h_bad : unknown metavariable '?_uniq.330'
h_bad : c + s s.length : unknown metavariable '?_uniq.330'
length > F . W ∨ i > F . W ) ( h : MeasRender F ( Doc.text s ) c i m ) :
Resolve ( Doc.text s ) c i ( MeasureSet.tainted : {α : Type } → Meas → MeasureSet m )
| text_set ( h_c : c + s s.length : unknown metavariable '?_uniq.507'
length ≤ F . W ) ( h_i : i ≤ F . W ) ( h : MeasRender F ( Doc.text s ) c i m ) :
Resolve ( Doc.text s ) c i ( MeasureSet.set : {α : Type } → (ms : List Meas ms ≠ [] MeasureSet [ m ] ( by simp ))
| align_taint ( h_bad : i > F . W ) ( h : Resolve d c c ms ) :
Resolve ( Doc.align d ) c i ( ms . taint : {α : Type } → MeasureSet → MeasureSet . lift : {α : Type } → (Meas → Meas MeasureSet → MeasureSet ( Meas.adjust_align : {α : Type } → ℕ → Meas → Meas i ))
| align ( h_ok : i ≤ F . W ) ( h : Resolve d c c ms ) :
Resolve ( Doc.align d ) c i ( ms . lift : {α : Type } → (Meas → Meas MeasureSet → MeasureSet ( Meas.adjust_align : {α : Type } → ℕ → Meas → Meas i ))
| nest ( h : Resolve d c (i + n ms h : Resolve d c ( i + n ) ms ) : Resolve ( Doc.nest n d ) c i ( ms . lift : {α : Type } → (Meas → Meas MeasureSet → MeasureSet ( Meas.adjust_nest : {α : Type } → ℕ → Meas → Meas n ))
| choice ( h_left : Resolve d c i ms ) ( h_right : Resolve d' c i ms'
h_right : Resolve d' c i ms' ) :
Resolve ( Doc.choice d d' ) c i ( MeasureSet.union : {α : Type } → Factory α MeasureSet → MeasureSet → MeasureSet F ms ms' )
| concat_taint ( h_left : Resolve d c i ( MeasureSet.tainted : {α : Type } → Meas → MeasureSet m )) ( h_right : Resolve d' m .lasti ms'
h_right : Resolve d' m . last : {α : Type } → Meas → ℕ i ms' ) ( h_taint : ms' . taint : {α : Type } → MeasureSet → MeasureSet = MeasureSet.tainted : {α : Type } → Meas → MeasureSet m' ) : ( Resolve ( Doc.concat d d' ) c i ( MeasureSet.tainted : {α : Type } → Meas → MeasureSet ( Meas.concat : {α : Type } → Factory α Meas → Meas → Meas F m m' )))
| concat_set ( h_left : Resolve d c i ( MeasureSet.set : {α : Type } → (ms : List Meas ms ≠ [] MeasureSet ms h_non_empty ))
( h : ResolveConcat ms d' i msr
h : ResolveConcat ms d' i msr ) :
Resolve ( Doc.concat d d' ) c i msr
inductive ResolveConcat : List Meas → Doc → ℕ → MeasureSet → Prop where
| one ( h_current : ResolveConcatOne d m i msr
h_current : ResolveConcatOne : Doc → Meas → ℕ → MeasureSet → Prop ResolveConcatOne d m i msr ) : ResolveConcat [ m ] d i msr
| cons ( h_rest : ResolveConcat ms d i msr
h_rest : ResolveConcat ms d i msr )
( h_current : ResolveConcatOne d m i msr'
h_current : ResolveConcatOne : Doc → Meas → ℕ → MeasureSet → Prop ResolveConcatOne d m i msr' ) :
ResolveConcat ( m :: ms ) d i ( MeasureSet.union : {α : Type } → Factory α MeasureSet → MeasureSet → MeasureSet F msr' msr )
inductive ResolveConcatOne : Doc → Meas → ℕ → MeasureSet → Prop ResolveConcatOne : Doc → Meas → ℕ → MeasureSet → Prop where
| tainted ( h : Resolve d m . last : {α : Type } → Meas → ℕ i ( MeasureSet.tainted : {α : Type } → Meas → MeasureSet m' )) :
ResolveConcatOne : Doc → Meas → ℕ → MeasureSet → Prop ResolveConcatOne d m i ( MeasureSet.tainted : {α : Type } → Meas → MeasureSet ( Meas.concat : {α : Type } → Factory α Meas → Meas → Meas F m m' ))
| set ( h : Resolve d m . last : {α : Type } → Meas → ℕ i ( MeasureSet.set : {α : Type } → (ms : List Meas ms ≠ [] MeasureSet ms h_non_empty )) :
ResolveConcatOne : Doc → Meas → ℕ → MeasureSet → Prop ResolveConcatOne d m i ( MeasureSet.set : {α : Type } → (ms : List Meas ms ≠ [] MeasureSet ( dedup F ( ms . map ( fun m' => Meas.concat : {α : Type } → Factory α Meas → Meas → Meas F m m' ))) ( by {
apply dedup_not_empty
simp [ h_non_empty ]
} ))
end
end Resolve