Cairn Docs Claims Blog Packages

Claim ยท cairn 0.2.2

cairn^109 Add an item, then delete it

A flow of cairn 0.2.2, in Basics window.

Id
cairn^109
Kind
flow
Reads as
proved
Place
Basics window ^106
Version
0.2.2

All of cairn 0.2.2's claims

What you do

Type milk, press Add, then press milk's delete button.

What you see

The list is empty again, and nothing is 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. press on ^102 Add
  3. press on ^104#1 Delete an item

Evidence

provedliveExamples.Basics.addThenDelete.live
provedreachesExamples.Basics.addThenDelete.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.addThenDelete
Module
Examples.Basics
Source
lean/Examples/Basics.lean:373 at v0.2.2
Machine
Examples.Basics.machine
Statement
Examples.Basics.addThenDelete.goal Examples.Basics.addThenDelete.witness
Statement hash
1ee050c6a434a9a5

Ledger

cairn^109 is active in this version's claims.lock, statement 1ee050c6a434a9a5. An id never moves or changes meaning.