Cairn Docs Claims Blog Packages

Claim ยท cairn 0.5.2

cairn^1010 The window is never smaller than the app's minimum size

An assumption of cairn 0.5.2.

Id
cairn^1010
Kind
assume
Reads as
assumed
Version
0.5.2

All of cairn 0.5.2's claims

What it says

The host sets the window's contentMinSize to the minimum size of the frame's window record (a negative side as 0), so a person can't drag it smaller, clamps every live resize AppKit proposes to it, and grows a window already smaller to it, keeping its top-left corner; a minimum the window meets leaves it alone. So every resize Lean hears is at least the minimum the app asked for, from the first frame that asks for it.

Evidence

assumedStated, not proved. The proofs rely on it.
fuzzedNot shown yet: the trusted-base fuzzer's check window.min-size held. A CI step will publish it (#95).

Where it's defined

Declaration
Cairn.Fuzz.Trusted.Claims.hostWindowMinSize
Module
Cairn.Fuzz.Trusted.Claims
Source
lean/Cairn/Fuzz/Trusted/Claims.lean:246 at v0.5.2
Statement hash
-

Ledger

cairn^1010 is active in this version's claims.lock. An id never moves or changes meaning.