Cairn · module
Cairn.Layout.Proofs
lean/Cairn/Layout/Proofs.lean
Layout theorems
The headline is Cairn.Layout.facts: for every valid metrics, window and view, layout
satisfies Facts. The pieces:
layout_controls: the controls of the laid tree are those of the view, in order.layout_childClips,layout_clipInside,layout_rootClip: clips nest, starting at the window.layout_siblingsDisjoint: children of rows and columns don't overlap.layout_fillExact: fill children make a row or column span its parent exactly.layout_caretPlaced: caret and selection geometry of every field.TextMetrics.mono_valid: the test metrics satisfyTextMetrics.Valid.
Each local fact is proved for a single arrange step and lifted to the whole tree by
arrange_everywhere, the one induction over the nested Sized tree.
Imports Cairn.Layout.Facts
Order
Definitions 7
controls : Sized → List Control
controlsList : List Sized → List Control
mainStart (h : Bool) (r : Rect) : Int
Start of a rect along the main axis.
mainPairs (h : Bool) (its : List Item) (rs : List Rect) : List (Sizing × Int)
Each child's main-axis sizing paired with its main-axis length.
crossStart (h : Bool) (r : Rect) : Int
Start and length of a rect across the main axis.
crossOf (h : Bool) (r : Rect) : Int
spSum (sp : Nat → Int) : Nat → Nat → Int
sp i + sp (i+1) + … + sp (i+n-1).
Theorems 117
paraLines_controls (m : TextMetrics) (ts : TextStyle) (wr : Wrap) (aw : Int) (s : String) : Sized.controlsList (paraLines m ts wr aw s) = []
A wrapped text's lines are text, so they have no controls.
measure_controls (m : TextMetrics) (aw : Int) (n : Node) : (measure m aw n).controls = n.controls
measureList_controls (m : TextMetrics) (aw : Int) (ns : List Node) : Sized.controlsList (measureList m aw ns) = Node.controlsList ns
arrange_controls (m : TextMetrics) (s : Sized) (c r : Rect) : (arrange m c r s).controls = s.controls
arrangeList_controls (m : TextMetrics) (ss : List Sized) (c : Rect) (rs : List Rect) : Laid.controlsList (arrangeList m c rs ss) = Sized.controlsList ss
layout_controls (m : TextMetrics) (w : Size) (n : Node) : (layout m w n).controls = n.controls
Controls preserved. The controls of the laid-out tree, in paint order, are exactly the controls of the view: none lost, none invented, none reordered.
arrange_rect (m : TextMetrics) (c r : Rect) (s : Sized) : (arrange m c r s).rect = r
arrange_clip (m : TextMetrics) (c r : Rect) (s : Sized) : (arrange m c r s).clip = c
arrange_sizings (m : TextMetrics) (c r : Rect) (s : Sized) : (arrange m c r s).sizings = s.sizings
arrange_children_box (m : TextMetrics) (c r : Rect) (st : Style) (ctl : Option Control) (sz : Size) (kids : List Sized) : (arrange m c r (Sized.box st ctl sz kids)).children = arrangeList m (innerClip st c r) (childRects st r (List.map Sized.item kids)) kids
arrange_children_nil (m : TextMetrics) (c r : Rect) (s : Sized) (h : ∀ (st : Style) (ctl : Option Control) (sz : Size) (kids : List Sized), s ≠ Sized.box st ctl sz kids) : (arrange m c r s).children = []
arrangeList_clip (m : TextMetrics) (c : Rect) (rs : List Rect) (ss : List Sized) (k : Laid) : k ∈ arrangeList m c rs ss → k.clip = c
arrangeList_length (m : TextMetrics) (c : Rect) (rs : List Rect) (ss : List Sized) : (arrangeList m c rs ss).length = ss.length
arrangeList_map {α : Type} (m : TextMetrics) (c : Rect)
(g : Sizing × Sizing → Rect → α) (rs : List Rect) (ss : List Sized) :
rs.length = ss.length →
List.map (fun k => g k.sizings k.rect) (arrangeList m c rs ss) =
List.zipWith (fun s r => g s.sizings r) ss rsWith one rect per child, each child lands in its rect.
arrangeList_rects (m : TextMetrics) (c : Rect) (rs : List Rect) (ss : List Sized) (h : rs.length = ss.length) : List.map Laid.rect (arrangeList m c rs ss) = rs
arrange_everywhere (m : TextMetrics) (P : Laid → Prop) (Q : Rect → Rect → Prop) (H : ∀ (c r : Rect) (s : Sized), Q c r → P (arrange m c r s) ∧ ∀ (k : Laid), k ∈ (arrange m c r s).children → Q k.clip k.rect) (s : Sized) (c r : Rect) : Q c r → Laid.Everywhere P (arrange m c r s)
The one induction over the tree. If every arrange step whose clip and rect satisfy Q
satisfies P and hands its children clips and rects satisfying Q, then P holds at every
node.
arrangeList_everywhere (m : TextMetrics) (P : Laid → Prop) (Q : Rect → Rect → Prop) (H : ∀ (c r : Rect) (s : Sized), Q c r → P (arrange m c r s) ∧ ∀ (k : Laid), k ∈ (arrange m c r s).children → Q k.clip k.rect) (ss : List Sized) (c : Rect) (rs : List Rect) : (∀ (k : Laid), k ∈ arrangeList m c rs ss → Q k.clip k.rect) → ∀ (k : Laid), k ∈ arrangeList m c rs ss → Laid.Everywhere P k
arrange_everywhere' (m : TextMetrics) (P : Laid → Prop) (H : ∀ (c r : Rect) (s : Sized), P (arrange m c r s)) (s : Sized) (c r : Rect) : Laid.Everywhere P (arrange m c r s)
The unconditional case.
inside_refl (r : Rect) : r.inside r
inside_trans {a b c : Rect} (hab : a.inside b) (hbc : b.inside c) :
a.inside c
inter_inside {a : Rect} (b : Rect) (hw : 0 ≤ a.w) (hh : 0 ≤ a.h) :
(a.inter b).inside a
inter_nonneg (a b : Rect) : 0 ≤ (a.inter b).w ∧ 0 ≤ (a.inter b).h
arrange_childClips (m : TextMetrics) (c r : Rect) (s : Sized) : ChildClips (arrange m c r s)
arrange_clipInside (m : TextMetrics) (c r : Rect) (s : Sized) (hw : 0 ≤ c.w) (hh : 0 ≤ c.h) : ClipInside (arrange m c r s) ∧ ∀ (k : Laid), k ∈ (arrange m c r s).children → 0 ≤ k.clip.w ∧ 0 ≤ k.clip.h
windowRect_nonneg (w : Size) : 0 ≤ (windowRect w).w ∧ 0 ≤ (windowRect w).h
layout_childClips (m : TextMetrics) (w : Size) (n : Node) : Laid.Everywhere ChildClips (layout m w n)
layout_clipInside (m : TextMetrics) (w : Size) (n : Node) : Laid.Everywhere ClipInside (layout m w n)
layout_rootClip (m : TextMetrics) (w : Size) (n : Node) : (layout m w n).clip = windowRect w
layout_rootOrigin (m : TextMetrics) (w : Size) (n : Node) : (layout m w n).rect.x = 0 ∧ (layout m w n).rect.y = 0
resolve_nonneg (s : Sizing) (x : Int) : 0 ≤ resolve s x
mainBase_nonneg (s : Sizing) (p : Int) : 0 ≤ mainBase s p
mainSize_nonneg (h : Bool) {L : Int} (hL : 0 ≤ L) (f j : Nat) (it : Item) : 0 ≤ mainSize h L f j it
crossPlace_nonneg (al : Align) (c0 : Int) {cc : Int} (hc : 0 ≤ cc) (s : Sizing) (p : Int) (b : Bool) : 0 ≤ (crossPlace al c0 cc s p b).snd
spacing_nonneg (j : Align) (gap : Nat) (free : Int) (k i : Nat) : 0 ≤ spacing j gap free k i
mkRect_mainStart (h : Bool) (p s cp cs : Int) : mainStart h (mkRect h p s cp cs) = p
mkRect_mainOf (h : Bool) (p s cp cs : Int) : mainOf h (mkRect h p s cp cs) = s
mkRect_nonneg (h : Bool) (p s cp cs : Int) (hs : 0 ≤ s) (hcs : 0 ≤ cs) : 0 ≤ (mkRect h p s cp cs).w ∧ 0 ≤ (mkRect h p s cp cs).h
go_length (ln : Line) (its : List Item) (i j : Nat) (pos : Int) : (ln.go i j pos its).length = its.length
go_nonneg (ln : Line) (hL : 0 ≤ ln.L) (hcc : 0 ≤ ln.cc) (its : List Item) (i j : Nat) (pos : Int) (r : Rect) : r ∈ ln.go i j pos its → 0 ≤ r.w ∧ 0 ≤ r.h
go_lower (ln : Line) (hL : 0 ≤ ln.L) (hsp : ∀ (i : Nat), 0 ≤ ln.spacing i) (its : List Item) (i j : Nat) (pos : Int) (r : Rect) : r ∈ ln.go i j pos its → pos ≤ mainStart ln.horiz r
go_pairwise (ln : Line) (hL : 0 ≤ ln.L) (hsp : ∀ (i : Nat), 0 ≤ ln.spacing i) (its : List Item) (i j : Nat) (pos : Int) : List.Pairwise (fun a b => mainStart ln.horiz a + mainOf ln.horiz a ≤ mainStart ln.horiz b) (ln.go i j pos its)
Along the main axis, each child ends before every later child starts.
disjoint_of_main (h : Bool) {a b : Rect} (hab : mainStart h a + mainOf h a ≤ mainStart h b) : a.disjoint b
leftover_nonneg (h : Bool) (st : Style) (c : Rect) (items : List Item) : 0 ≤ leftover h st c items
lineRects_length (h : Bool) (st : Style) (c : Rect) (items : List Item) : (lineRects h st c items).length = items.length
lineRects_nonneg (h : Bool) (st : Style) (c : Rect) (items : List Item) (r : Rect) : r ∈ lineRects h st c items → 0 ≤ r.w ∧ 0 ≤ r.h
lineRects_pairwise (h : Bool) (st : Style) (c : Rect) (items : List Item) : List.Pairwise (fun a b => a.disjoint b) (lineRects h st c items)
scrollBy_w (h : Bool) (o : Int) (q : Rect) : (scrollBy h o q).w = q.w
scrollBy_h (h : Bool) (o : Int) (q : Rect) : (scrollBy h o q).h = q.h
mainOf_scrollBy (h h' : Bool) (o : Int) (q : Rect) : mainOf h (Rect.scrollBy h' o q) = mainOf h q
scrollBy_disjoint (h : Bool) (o : Int) {a b : Rect} (hd : a.disjoint b) : (scrollBy h o a).disjoint (scrollBy h o b)
scrolled_length (st : Style) (rs : List Rect) : (scrolled st rs).length = rs.length
mem_scrolled {st : Style} {rs : List Rect} {q : Rect}
(hq : q ∈ scrolled st rs) : ∃ q', q' ∈ rs ∧ q.w = q'.w ∧ q.h = q'.h
scrolled_pairwise (st : Style) {rs : List Rect} (h : List.Pairwise (fun a b => a.disjoint b) rs) : List.Pairwise (fun a b => a.disjoint b) (scrolled st rs)
scrolled_none {st : Style} (h : st.scroll = none) (rs : List Rect) :
scrolled st rs = rs
map_mainOf_scrolled (h : Bool) (st : Style) (rs : List Rect) : List.map (mainOf h) (scrolled st rs) = List.map (mainOf h) rs
placeRects_length (st : Style) (r : Rect) (items : List Item) : (placeRects st r items).length = items.length
childRects_length (st : Style) (r : Rect) (items : List Item) : (childRects st r items).length = items.length
placeRects_nonneg (st : Style) (r : Rect) (items : List Item) (q : Rect) : q ∈ placeRects st r items → 0 ≤ q.w ∧ 0 ≤ q.h
childRects_nonneg (st : Style) (r : Rect) (items : List Item) (q : Rect) : q ∈ childRects st r items → 0 ≤ q.w ∧ 0 ≤ q.h
placeRects_line (st : Style) (r : Rect) (items : List Item) (hax : st.axis ≠ Axis.stack) : placeRects st r items = lineRects (Axis.horiz st.axis) st (r.inset st.padding) items
childRects_pairwise (st : Style) (r : Rect) (items : List Item) (hax : st.axis ≠ Axis.stack) : List.Pairwise (fun a b => a.disjoint b) (childRects st r items)
kid_rect_mem {m : TextMetrics} {c : Rect} {rs : List Rect} {ss : List Sized}
(h : rs.length = ss.length) {k : Laid} (hk : k ∈ arrangeList m c rs ss) : k.rect ∈ rs
arrange_rectNonneg (m : TextMetrics) (c r : Rect) (s : Sized) (hw : 0 ≤ r.w) (hh : 0 ≤ r.h) : RectNonneg (arrange m c r s) ∧ ∀ (k : Laid), k ∈ (arrange m c r s).children → 0 ≤ k.rect.w ∧ 0 ≤ k.rect.h
measure_size_nonneg (m : TextMetrics) (aw : Int) (n : Node) : 0 ≤ (measure m aw n).size.w ∧ 0 ≤ (measure m aw n).size.h
layout_rectNonneg (m : TextMetrics) (w : Size) (n : Node) : Laid.Everywhere RectNonneg (layout m w n)
arrange_siblingsDisjoint (m : TextMetrics) (c r : Rect) (s : Sized) : SiblingsDisjoint (arrange m c r s)
layout_siblingsDisjoint (m : TextMetrics) (w : Size) (n : Node) : Laid.Everywhere SiblingsDisjoint (layout m w n)
Siblings disjoint. In every row and column of the laid-out tree, distinct children's rects are disjoint (earlier children end before later ones start on the main axis).
get {r c : Rect} {st : Style} {ctl : Option Control}
{kids : List Laid} (h : SiblingsDisjoint (Laid.box r c st ctl kids))
(hax : st.axis ≠ Axis.stack) {i j : Nat} (hi : i < kids.length) (hj : j < kids.length)
(hij : i ≠ j) : kids[i].rect.disjoint kids[j].rectThe index form: children i ≠ j of a row or column have disjoint rects.
go_fill (ln : Line) (its : List Item) (i j : Nat) (pos : Int) : (List.map (fun x => x.snd) (List.filter (fun x => !x.fst.isFill) (mainPairs ln.horiz its (ln.go i j pos its)))).sum = baseSum ln.horiz its ∧ (List.map (fun x => x.snd) (mainPairs ln.horiz its (ln.go i j pos its))).sum = baseSum ln.horiz its + (cumShare ln.L ln.f (j + fillCount ln.horiz its) - cumShare ln.L ln.f j) ∧ (((mainPairs ln.horiz its (ln.go i j pos its)).any fun x => x.fst.isFill) = true → 0 < fillCount ln.horiz its)
lineRects_fill (h : Bool) (st : Style) (c : Rect) (items : List Item) (hany : ((mainPairs h items (lineRects h st c items)).any fun x => x.fst.isFill) = true) (hle : (List.map (fun x => x.snd) (List.filter (fun x => !x.fst.isFill) (mainPairs h items (lineRects h st c items)))).sum + gaps st.gap items.length ≤ mainOf h c) : (List.map (fun x => x.snd) (mainPairs h items (lineRects h st c items))).sum + gaps st.gap items.length = mainOf h c
Fill exactness for one line, in terms of its content box.
mainOf_inset (h : Bool) (r : Rect) (p : Insets) : mainOf h (r.inset p) = mainOf h r - padMain h p
arrange_fillExact (m : TextMetrics) (c r : Rect) (s : Sized) : FillExact (arrange m c r s)
layout_fillExact (m : TextMetrics) (w : Size) (n : Node) : Laid.Everywhere FillExact (layout m w n)
Fill exactness. In every row and column of the laid-out tree with a fill child, if the other children, gaps and padding fit, then children, gaps and padding span the parent exactly along the main axis.
offAt_eq (offs : Array Int) {i : Nat} (h : i < offs.size) : offAt offs i = offs[i]
offAt_bounds {m : TextMetrics} (hm : m.Valid) (f : Font) (s : String)
(i : Nat) : 0 ≤ offAt (m.offsets f s) i ∧ offAt (m.offsets f s) i ≤ m.width f sUnder valid metrics every caret offset lies between 0 and the text's width.
arrange_caretPlaced {m : TextMetrics} (hm : m.Valid) (c r : Rect) (s : Sized) :
CaretPlaced m (arrange m c r s)
layout_caretPlaced {m : TextMetrics} (hm : m.Valid) (w : Size) (n : Node) :
Laid.Everywhere (CaretPlaced m) (layout m w n)Caret placement. In every field of the laid-out tree, the caret's x is the text origin plus the caret's offset, lies within the text's extent, and lies inside the content box whenever the box is at least a point wide; the selection runs between the offsets of its ends.
mono_valid : mono.Valid
mkRect_crossStart (h : Bool) (p s cp cs : Int) : crossStart h (mkRect h p s cp cs) = cp
mkRect_crossOf (h : Bool) (p s cp cs : Int) : crossOf h (mkRect h p s cp cs) = cs
crossOf_scrollBy (h h' : Bool) (o : Int) (q : Rect) : crossOf h (Rect.scrollBy h' o q) = crossOf h q
spSum_nonneg (sp : Nat → Int) (hsp : ∀ (i : Nat), 0 ≤ sp i) (i n : Nat) : 0 ≤ spSum sp i n
spSum_const (sp : Nat → Int) (g : Nat) (hsp : ∀ (i : Nat), sp i = ↑g) (i n : Nat) : spSum sp i n = ↑(g * n)
spSum_tele (sp : Nat → Int) (g : Nat) (F : Nat → Int) (hsp : ∀ (i : Nat), sp i = ↑g + (F (i + 1) - F i)) (i n : Nat) : spSum sp i n = ↑(g * n) + (F (i + n) - F i)
sum_nonneg (l : List Int) (h : ∀ (x : Int), x ∈ l → 0 ≤ x) : 0 ≤ l.sum
go_mainOf_nonneg (ln : Line) (hL : 0 ≤ ln.L) (its : List Item) (i j : Nat) (pos : Int) : 0 ≤ (List.map (mainOf ln.horiz) (ln.go i j pos its)).sum
go_upper (ln : Line) (hL : 0 ≤ ln.L) (hsp : ∀ (i : Nat), 0 ≤ ln.spacing i) (its : List Item) (i j : Nat) (pos : Int) (r : Rect) : r ∈ ln.go i j pos its → mainStart ln.horiz r + mainOf ln.horiz r ≤ pos + (List.map (mainOf ln.horiz) (ln.go i j pos its)).sum + spSum ln.spacing i (its.length - 1)
Along the main axis, every child ends by the start plus all lengths and spacings.
crossPlace_inside (al : Align) (c0 cc : Int) (s : Sizing) (p : Int) (b : Bool) (h : (crossPlace al c0 cc s p b).snd ≤ cc) : c0 ≤ (crossPlace al c0 cc s p b).fst ∧ (crossPlace al c0 cc s p b).fst + (crossPlace al c0 cc s p b).snd ≤ c0 + cc
go_cross (ln : Line) (its : List Item) (i j : Nat) (pos : Int) (r : Rect) : r ∈ ln.go i j pos its → crossOf ln.horiz r ≤ ln.cc → ln.c0 ≤ crossStart ln.horiz r ∧ crossStart ln.horiz r + crossOf ln.horiz r ≤ ln.c0 + ln.cc
mainPairs_snd (h : Bool) (its : List Item) (rs : List Rect) : its.length = rs.length → List.map (fun x => x.snd) (mainPairs h its rs) = List.map (mainOf h) rs
lineRects_sum (h : Bool) (st : Style) (c : Rect) (items : List Item) : (List.map (mainOf h) (lineRects h st c items)).sum = if fillCount h items = 0 then baseSum h items else baseSum h items + leftover h st c items
The children's main-axis lengths add up to the space the line uses.
lineRects_inside (h : Bool) (st : Style) (c : Rect) (items : List Item) (hcross : ∀ (r : Rect), r ∈ lineRects h st c items → crossOf h r ≤ crossOf h c) (hfit : (List.map (mainOf h) (lineRects h st c items)).sum + gaps st.gap items.length ≤ mainOf h c) (r : Rect) : r ∈ lineRects h st c items → r.inside c
stackRects_inside (st : Style) (c : Rect) (items : List Item) (hfit : ∀ (r : Rect), r ∈ stackRects st c items → r.w ≤ c.w ∧ r.h ≤ c.h) (r : Rect) : r ∈ stackRects st c items → r.inside c
arrange_childrenInside (m : TextMetrics) (c r : Rect) (s : Sized) : ChildrenInside (arrange m c r s)
layout_childrenInside (m : TextMetrics) (w : Size) (n : Node) : Laid.Everywhere ChildrenInside (layout m w n)
Children that fit stay inside. In every container of the laid-out tree, if the children fit the content box (in size, and along the main axis with gaps), each child's rect is inside it.
placeRects_scroll (st : Style) (s : Option Int) (r : Rect) (items : List Item) : placeRects { axis := st.axis, width := st.width, height := st.height, padding := st.padding, gap := st.gap, align := st.align, justify := st.justify, background := st.background, border := st.border, radius := st.radius, clip := st.clip, corner := st.corner, shadow := st.shadow, paint := st.paint, image := st.image, scroll := s, scrollRef := st.scrollRef, rows := st.rows, menu := st.menu } r items = placeRects st r items
childRects_scroll {st : Style} {o : Int} (ho : st.scroll = some o) (r : Rect)
(items : List Item) :
childRects st r items =
List.map (Rect.scrollBy (Axis.horiz st.axis) o)
(childRects
{ axis := st.axis, width := st.width, height := st.height, padding := st.padding,
gap := st.gap, align := st.align, justify := st.justify,
background := st.background, border := st.border, radius := st.radius,
clip := st.clip, corner := st.corner, shadow := st.shadow, paint := st.paint,
image := st.image, scrollRef := st.scrollRef, rows := st.rows, menu := st.menu }
r items)A scroll box's children are where the same box without scroll puts them (placeRects:
in a column, one under the other), moved back by the offset along the box's axis.
arrange_scroll (m : TextMetrics) (c r : Rect) {st : Style} (ctl : Option Control) (sz : Size) (kids : List Sized) {o : Int} (ho : st.scroll = some o) : List.map Laid.rect (arrange m c r (Sized.box st ctl sz kids)).children = List.map (Rect.scrollBy (Axis.horiz st.axis) o) (List.map Laid.rect (arrange m c r (Sized.box { axis := st.axis, width := st.width, height := st.height, padding := st.padding, gap := st.gap, align := st.align, justify := st.justify, background := st.background, border := st.border, radius := st.radius, clip := st.clip, corner := st.corner, shadow := st.shadow, paint := st.paint, image := st.image, scrollRef := st.scrollRef, rows := st.rows, menu := st.menu } ctl sz kids)).children)
Scrolled children. Every child of a scroll box with offset o is laid at the rect the
same box gives it when it doesn't scroll, moved back by o along the box's axis: in a column (or
a stack), the same x, width and height, and y less o; in a row, x less o.
measure_scroll (m : TextMetrics) (aw : Int) (st : Style) (s : Option Int) (ctl : Option Control) (kids : List Node) : measure m aw (Node.box { axis := st.axis, width := st.width, height := st.height, padding := st.padding, gap := st.gap, align := st.align, justify := st.justify, background := st.background, border := st.border, radius := st.radius, clip := st.clip, corner := st.corner, shadow := st.shadow, paint := st.paint, image := st.image, scroll := s, scrollRef := st.scrollRef, rows := st.rows, menu := st.menu } ctl kids) = Sized.box { axis := st.axis, width := st.width, height := st.height, padding := st.padding, gap := st.gap, align := st.align, justify := st.justify, background := st.background, border := st.border, radius := st.radius, clip := st.clip, corner := st.corner, shadow := st.shadow, paint := st.paint, image := st.image, scroll := s, scrollRef := st.scrollRef, rows := st.rows, menu := st.menu } ctl (measure m aw (Node.box st ctl kids)).size (measureList m (innerAvail st aw) kids)
Measuring doesn't read scroll: a box measures the same with any offset, or none.
scrollBy_column (o : Int) (q : Rect) : Rect.scrollBy false o q = { x := q.x, y := q.y - o, w := q.w, h := q.h }
In a column, scrolling by o moves a rect up by o and changes nothing else.
and {P Q : Laid → Prop} {l : Laid} (hp : Everywhere P l)
(hq : Everywhere Q l) : Everywhere (fun x => P x ∧ Q x) l
imp {P Q : Laid → Prop} {l : Laid} (hp : Everywhere P l)
(f : ∀ (x : Laid), P x → Q x) : Everywhere Q l
tails {P : Laid → Prop} {l : Laid} (hp : Everywhere P l) :
Everywhere (fun d => Everywhere P d) lA fact holding everywhere holds everywhere at every node's subtree.
inter_inside_of_nonempty {a b : Rect} (h : (a.inter b).nonempty) :
(a.inter b).inside b
nonempty_of_inside {a b : Rect} (hi : a.inside b) (h : a.nonempty) :
b.nonempty
clip_inside_everywhere {R : Rect} {l : Laid}
(hE : Laid.Everywhere ClipInside l) :
l.clip.inside R → Laid.Everywhere (fun d => d.clip.inside R) lClips only shrink going down: below a node whose clip is inside R, every clip is.
visible_inside_clip {d : Laid} (h : d.visible.nonempty) :
d.visible.inside d.clipA nonempty visible part lies inside the node's clip.
clipContained_of {l : Laid} (hE : Laid.Everywhere ClipInside l)
(hcc : ChildClips l) : ClipContained l
layout_clipContained (m : TextMetrics) (w : Size) (n : Node) : Laid.Everywhere ClipContained (layout m w n)
Clips hold what is under them. In every box of the laid-out tree that clips, so in every scroll box, every nonempty visible part of every node below it is inside the box's rect.
facts {m : TextMetrics} (hm : m.Valid) (w : Size) (n : Node) :
Facts m w n (layout m w n)
measure_image (m : TextMetrics) (aw : Int) (i : Image) : (measure m aw (Node.image i)).size = { w := ↑i.width, h := ↑i.height }
An image's box doesn't depend on its state. Node.image measures at the size the app
gave it whether it is loading, loaded at any pixel size, or failed, so nothing around it moves
when the pixels arrive or the load fails.
image_sizings (m : TextMetrics) (aw : Int) (i : Image) : (measure m aw (Node.image i)).sizings = (Sizing.fixed i.width, Sizing.fixed i.height)
An image's size is fixed on both axes, so rows and columns never stretch or shrink it.
controls_image (i : Image) : (Node.image i).controls = []
An image is no control, in any state.