Cairn Docs Claims Blog Packages

Claim ยท cairn 0.5.2

cairn^947 The host shows a control menu only while Lean has it open

An assumption of cairn 0.5.2.

Id
cairn^947
Kind
assume
Reads as
assumed
Version
0.5.2

All of cairn 0.5.2's claims

What it says

The host shows a control's menu exactly when the last frame shows one, except that after the host closed it, a frame that does not yet account for that close (its events are numbered below the close) does not open it again; a frame without the menu, or without a window, dismisses one that is open.

Evidence

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

Where it's defined

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

Ledger

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