Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^319 Fixes replace whole words

An invariant of yap 0.1.0.

Id
yap^319
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

What is typed is the text of a successful transcription reply with each dictionary fix applied to whole words only, case-insensitively, then trimmed, then a space (or Return) (`app_typed_text`, `typed_text`, `replaceWord_replaces`).

Evidence

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

Ledger

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