Cairn Docs Claims Blog Packages

Claim ยท cairn_examples 0.2.0

cairn_examples^4 Count to three

A flow of cairn_examples 0.2.0, in Counter window.

Id
cairn_examples^4
Kind
flow
Reads as
proved
Place
Counter window ^3
Version
0.2.0

All of cairn_examples 0.2.0's claims

What you do

Press Increment three times.

What you see

The count is three.

Steps

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

  1. press on ^1 Increment
  2. press on ^1 Increment
  3. press on ^1 Increment

Evidence

provedliveExamples.Counter.countToThree.live
provedreachesExamples.Counter.countToThree.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.Counter.countToThree
Module
Counter
Source
lean/Counter.lean:75 at v0.2.0
Machine
Examples.Counter.machine
Statement
Examples.Counter.countToThree.goal Examples.Counter.countToThree.witness
Statement hash
8e8ea87eb87cc917

Ledger

cairn_examples^4 is active in this version's claims.lock, statement 8e8ea87eb87cc917. An id never moves or changes meaning.