Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^946 Choosing a control menu's item reports its ref, then the close
An assumption of cairn 0.5.2.
- Id
cairn^946- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
When AppKit performs an item's action in a control's menu, the host sends exactly one menuSelect with the window's place and that item's ref, and nothing for a status line, separator or submenu; when the menu closes, chosen from or not, it sends one menuClose with the window's place, after any menuSelect.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check control-menu.select held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostControlMenuSelect- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:180atv0.5.2- Statement hash
-
Ledger
cairn^946 is active in this version's claims.lock. An id never moves or changes meaning.