Cairn Docs Claims Blog Packages

Claim ยท cairn_examples 0.2.0

cairn_examples^223 Mark all as complete, then undo it

A flow of cairn_examples 0.2.0, in Todos window.

Id
cairn_examples^223
Kind
flow
Reads as
proved
Place
Todos window ^201
Version
0.2.0

All of cairn_examples 0.2.0's claims

What you do

Add milk and eggs, check milk, press toggle all twice.

What you see

After the first press every todo is completed and the counter says 0 items left; after the second every todo is active again (T16, T35).

Steps

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

  1. edit insert "milk" on ^202 New todo
  2. submit on ^202 New todo
  3. edit insert "eggs" on ^202 New todo
  4. submit on ^202 New todo
  5. press on ^204#1 Complete a todo
  6. press on ^203 Mark all as complete
  7. press on ^203 Mark all as complete

Evidence

provedliveExamples.Todo.markAllComplete.live
provedreachesExamples.Todo.markAllComplete.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.Todo.markAllComplete
Module
Todo
Source
lean/Todo.lean:270 at v0.2.0
Machine
Examples.Todo.machine
Statement
Examples.Todo.markAllComplete.goal Examples.Todo.markAllComplete.witness
Statement hash
36d2b8e708c4eceb

Ledger

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