Cairn Docs Claims Blog Packages

Claim ยท cairn_examples 0.2.0

cairn_examples^462 Add an item and pick it

A flow of cairn_examples 0.2.0, in Tray menu.

Id
cairn_examples^462
Kind
flow
Reads as
proved
Place
Tray menu ^450
Version
0.2.0

All of cairn_examples 0.2.0's claims

What you do

Choose Add Item, then the new item under Recent Items.

What you see

The status line names the new item.

Steps

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

  1. press on ^456 Add Item
  2. press on ^457 Recent item

Evidence

provedliveExamples.Tray.addAndPick.live
provedreachesExamples.Tray.addAndPick.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.Tray.addAndPick
Module
Tray
Source
lean/Tray.lean:189 at v0.2.0
Machine
Examples.Tray.machine
Statement
Examples.Tray.addAndPick.goal Examples.Tray.addAndPick.witness
Statement hash
fbb1f497f8493322

Ledger

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