Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^945 A control's menu shows exactly the frame's menu records
An assumption of cairn 0.5.2.
- Id
cairn^945- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
While the window's frame record shows a control's menu (its status: the owner and the menu records), the host's native menu for it holds those records as a status item's does (^940), for that owner, at the window's place; a frame with no menu records shows none.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check control-menu.render held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostControlMenuRender- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:176atv0.5.2- Statement hash
-
Ledger
cairn^945 is active in this version's claims.lock. An id never moves or changes meaning.