Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^1000 openItem opens exactly the URL or existing file it names
An assumption of cairn 0.5.2.
- Id
cairn^1000- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
openItem with a target that has a URL scheme asks the system to open that URL; with a path (a leading ~/ is the home folder) it opens that file or folder with its default app only when it exists, and answers notFound otherwise; it answers done exactly when the system took it, and an empty target or one with NUL is invalid and opens nothing.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check effects.open-item held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostOpenItem- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:202atv0.5.2- Statement hash
-
Ledger
cairn^1000 is active in this version's claims.lock. An id never moves or changes meaning.