Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^316 A failed type is kept and flagged

An invariant of yap 0.1.0.

Id
yap^316
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

When typing fails, the transcript is first in Recent Transcripts (so Copy Last Transcript copies it), marked as never having reached its app, and the error sound plays (`app_failed_type_flagged`).

Evidence

provedinitYap.failedTypeFlagged.init
provedstepYap.failedTypeFlagged.step
provedreceiveYap.failedTypeFlagged.receive
provedreachableYap.failedTypeFlagged.reachable
provedreachableAllYap.failedTypeFlagged.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.failedTypeFlagged
Module
Yap
Source
lean/Yap.lean:321 at v0.1.0
Machine
Yap.machine
Statement
Yap.failedTypeFlagged.holds
Statement hash
323a175fac241715

Ledger

yap^316 is active in this version's claims.lock, statement 323a175fac241715. An id never moves or changes meaning.