Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^335 The host types into the app it was given

An assumption of yap 0.1.0.

Id
yap^335
Kind
assume
Reads as
assumed
Version
0.1.0

All of yap 0.1.0's claims

What it says

The host brings the app with the given process forward and types the text, then Return if asked; it replies failed when it can't (no Accessibility access, the app is gone), and ok only when the text was typed.

Evidence

assumedStated, not proved. The proofs rely on it.
fuzzedNot shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).

Where it's defined

Declaration
Yap.hostTypes
Module
Yap
Source
lean/Yap.lean:444 at v0.1.0
Statement hash
-

Ledger

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