Cairn Docs Claims Blog Packages

Claim ยท cairn_examples 0.2.0

cairn_examples^408 Start over

A flow of cairn_examples 0.2.0, in Clock window.

Id
cairn_examples^408
Kind
flow
Reads as
proved
Place
Clock window ^406
Version
0.2.0

All of cairn_examples 0.2.0's claims

What you do

Press Start, Lap, Stop, then Reset.

What you see

The reading is zero and no laps are listed.

Steps

The witness its liveness proof follows, from the app's first state.

  1. press on ^401 Start / Stop
  2. press on ^402 Lap
  3. press on ^401 Start / Stop
  4. press on ^403 Reset

Evidence

provedliveExamples.Clock.startOver.live
provedreachesExamples.Clock.startOver.reaches
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).
seenNot shown yet: a screenshot of the app shows it. A CI step will publish it (#95).

Where it's defined

Declaration
Examples.Clock.startOver
Module
Clock
Source
lean/Clock.lean:269 at v0.2.0
Machine
Examples.Clock.machine
Statement
Examples.Clock.startOver.goal Examples.Clock.startOver.witness
Statement hash
81892d4491fba6ac

Ledger

cairn_examples^408 is active in this version's claims.lock, statement 81892d4491fba6ac. An id never moves or changes meaning.