Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^330 The host reports the dictation key and every other key

An assumption of yap 0.1.0.

Id
yap^330
Kind
assume
Reads as
assumed
Version
0.1.0

All of yap 0.1.0's claims

What it says

The host reports the dictation key going down and up, once each per press, with its monotonic clock in milliseconds, and reports every other key that goes down while the dictation key is held, before the dictation key's release. Key repeats are not reported as presses.

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.hostKeys
Module
Yap
Source
lean/Yap.lean:429 at v0.1.0
Statement hash
-

Ledger

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