Cairn Docs Claims Blog Packages

Claim ยท cairn 0.2.4

cairn^220 Escape cancels an edit

A flow of cairn 0.2.4, in Todos window.

Id
cairn^220
Kind
flow
Reads as
proved
Place
Todos window ^201
Version
0.2.4

All of cairn 0.2.4's claims

What you do

Add milk, double-click it, delete its text, press Escape.

What you see

The title is still milk, and edit mode has ended (T31).

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. doublePress on ^205#1 Edit a todo
  4. edit selectAll on ^207#1 Edit field
  5. edit deleteBackward on ^207#1 Edit field
  6. cancel on ^207#1 Edit field

Evidence

provedliveExamples.Todo.escapeCancels.live
provedreachesExamples.Todo.escapeCancels.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.escapeCancels
Module
Examples.Todo
Source
lean/Examples/Todo.lean:247 at v0.2.4
Machine
Examples.Todo.machine
Statement
Examples.Todo.escapeCancels.goal Examples.Todo.escapeCancels.witness
Statement hash
b646e7f81edd3bef

Ledger

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