Cairn Docs Claims Blog Packages

Claim ยท cairn_examples 0.2.0

cairn_examples^224 A new todo under the Completed filter

A flow of cairn_examples 0.2.0, in Todos window.

Id
cairn_examples^224
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, press Completed, add eggs.

What you see

Eggs is created but not listed, since it is active; the filter stays Completed (T11, T12).

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. press on ^210 Completed
  4. edit insert "eggs" on ^202 New todo
  5. submit on ^202 New todo

Evidence

provedliveExamples.Todo.addUnderCompleted.live
provedreachesExamples.Todo.addUnderCompleted.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.addUnderCompleted
Module
Todo
Source
lean/Todo.lean:277 at v0.2.0
Machine
Examples.Todo.machine
Statement
Examples.Todo.addUnderCompleted.goal Examples.Todo.addUnderCompleted.witness
Statement hash
06954be5c9e714a8

Ledger

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