Cairn
Docs
Claims
Blog
Packages
Claim ยท yap 0.1.0
yap^340 Turn Dictate with Key off
A flow of yap 0.1.0, in Menu bar menu.
- Id
yap^340- Kind
- flow
- Reads as
- proved
- Place
- Menu bar menu
^301 - Version
- 0.1.0
What you do
Choose Dictate with Key.
What you see
Dictation is off, Press Return After Dictating is unavailable, and nothing is recording.
Steps
The witness its liveness proof follows, from the app's first state.
- press on
^306Dictate with Key
Evidence
| proved | live | Yap.turnOff.live |
| proved | reaches | Yap.turnOff.reaches |
| tested | Not shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95). | |
| seen | Not shown yet: a screenshot of the app shows it. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Yap.turnOff- Module
Yap- Source
lean/Yap.lean:458atv0.1.0- Machine
Yap.machine- Statement
Yap.turnOff.goalYap.turnOff.witness- Statement hash
74c5d55d256ee73f
Ledger
yap^340 is active in this version's claims.lock, statement 74c5d55d256ee73f. An id never moves or changes meaning.