Cairn Docs Claims Blog Packages

Claim ยท cairn 0.2.3

cairn^216 Add two todos and complete one

A flow of cairn 0.2.3, in Todos window.

Id
cairn^216
Kind
flow
Reads as
proved
Place
Todos window ^201
Version
0.2.3

All of cairn 0.2.3's claims

What you do

Type milk and press Enter, type eggs with spaces around it and press Enter, then check milk.

What you see

Two todos in order, eggs trimmed, milk completed, the field empty, and 1 item left.

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

Evidence

provedliveExamples.Todo.addAndComplete.live
provedreachesExamples.Todo.addAndComplete.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.addAndComplete
Module
Examples.Todo
Source
lean/Examples/Todo.lean:217 at v0.2.3
Machine
Examples.Todo.machine
Statement
Examples.Todo.addAndComplete.goal Examples.Todo.addAndComplete.witness
Statement hash
059a40708193b6f5

Ledger

cairn^216 is active in this version's claims.lock, statement 059a40708193b6f5. An id never moves or changes meaning.