Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^315 Kept before it is typed

An invariant of yap 0.1.0.

Id
yap^315
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

When Yap types a transcript, it is already in Recent Transcripts, marked not yet typed, and when transcripts are kept the request appending it to its day file comes before the request typing it (`app_saved_before_typed`, `saved_before_typed`). Swift Yap saves after typing; see the README.

Evidence

provedinitYap.keptBeforeTyped.init
provedstepYap.keptBeforeTyped.step
provedreceiveYap.keptBeforeTyped.receive
provedreachableYap.keptBeforeTyped.reachable
provedreachableAllYap.keptBeforeTyped.reachableAll
fuzzedNot shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).
testedNot shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95).

Where it's defined

Declaration
Yap.keptBeforeTyped
Module
Yap
Source
lean/Yap.lean:309 at v0.1.0
Machine
Yap.machine
Statement
Yap.keptBeforeTyped.holds
Statement hash
74b8e2c952548c59

Ledger

yap^315 is active in this version's claims.lock, statement 74b8e2c952548c59. An id never moves or changes meaning.