Cairn Docs Claims Blog Packages

Claim ยท cairn_examples 0.2.0

cairn_examples^107 Add two items and finish one

A flow of cairn_examples 0.2.0, in Basics window.

Id
cairn_examples^107
Kind
flow
Reads as
proved
Place
Basics window ^106
Version
0.2.0

All of cairn_examples 0.2.0's claims

What you do

Type milk and press Enter, type eggs and press Add, then check milk.

What you see

Two items, milk done, and one item left.

Steps

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

  1. edit insert "milk" on ^101 Type a new item
  2. submit on ^101 Type a new item
  3. edit insert " eggs " on ^101 Type a new item
  4. press on ^102 Add
  5. press on ^103#1 Toggle an item

Evidence

provedliveExamples.Basics.addAndFinish.live
provedreachesExamples.Basics.addAndFinish.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.Basics.addAndFinish
Module
Basics
Source
lean/Basics.lean:359 at v0.2.0
Machine
Examples.Basics.machine
Statement
Examples.Basics.addAndFinish.goal Examples.Basics.addAndFinish.witness
Statement hash
ed3fc7beee378157

Ledger

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