Cairn Docs Claims Blog Packages

Claim ยท cairn_examples 0.2.0

cairn_examples^221 The Active filter hides completed todos

A flow of cairn_examples 0.2.0, in Todos window.

Id
cairn_examples^221
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 Active.

What you see

Only eggs is listed, and the counter still says 1 item left (T40, T42).

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 ^209 Active

Evidence

provedliveExamples.Todo.activeFilter.live
provedreachesExamples.Todo.activeFilter.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.activeFilter
Module
Todo
Source
lean/Todo.lean:256 at v0.2.0
Machine
Examples.Todo.machine
Statement
Examples.Todo.activeFilter.goal Examples.Todo.activeFilter.witness
Statement hash
251baf03d4d2fb06

Ledger

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