Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn_examples 0.2.0
cairn_examples^406 Clock window
A place of cairn_examples 0.2.0.
- Id
cairn_examples^406- Kind
- place
- Reads as
- no proof
- Version
- 0.2.0
What it is
The stopwatch's window: the reading, the time of day, Start/Stop, Lap, Reset, Save laps, Load laps, a status line and the laps.
In this place
Moves
| Id | Claim | Reads as |
|---|---|---|
cairn_examples^401 | Start / StopPress Start (Stop while running). | proved |
cairn_examples^402 | LapPress Lap while the stopwatch runs. | proved |
cairn_examples^403 | ResetPress Reset while stopped. | proved |
cairn_examples^404 | Save lapsPress Save laps. | proved |
cairn_examples^405 | Load lapsPress Load laps. | proved |
Flows
| Id | Claim | Reads as |
|---|---|---|
cairn_examples^407 | Two lapsPress Start, then Lap twice. | proved |
cairn_examples^408 | Start overPress Start, Lap, Stop, then Reset. | proved |
Evidence
| no proof | A place states where claims live; it has nothing to prove. | |
| seen | Not shown yet: a screenshot of the app shows it. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Examples.Clock.window- Module
Clock- Source
lean/Clock.lean:102atv0.2.0- Statement hash
-
Ledger
cairn_examples^406 is active in this version's claims.lock. An id never moves or changes meaning.