Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.2.3
cairn^406 Clock window
A place of cairn 0.2.3.
- Id
cairn^406- Kind
- place
- Reads as
- no proof
- Version
- 0.2.3
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^401 | Start / StopPress Start (Stop while running). | proved |
cairn^402 | LapPress Lap while the stopwatch runs. | proved |
cairn^403 | ResetPress Reset while stopped. | proved |
cairn^404 | Save lapsPress Save laps. | proved |
cairn^405 | Load lapsPress Load laps. | proved |
Flows
| Id | Claim | Reads as |
|---|---|---|
cairn^407 | Two lapsPress Start, then Lap twice. | proved |
cairn^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
Examples.Clock- Source
lean/Examples/Clock.lean:102atv0.2.3- Statement hash
-
Ledger
cairn^406 is active in this version's claims.lock. An id never moves or changes meaning.