cairn_examples^207 Edit field

What you do

In edit mode, type in the todo's field; then press Enter, click elsewhere or Tab away, or press Escape. (T28–T31, T50)

What you see

Enter, a click elsewhere and Tab save: the trimmed text becomes the title, or the todo is deleted when it is blank. Escape leaves the title exactly as it was. Edit mode ends either way; after Enter or Escape keyboard focus returns to the new-todo field.

Evidence

proved	sound edit	`Examples.Todo.editTodo.edit.sound`
proved	sound submit	`Examples.Todo.editTodo.submit.sound`
proved	sound blur	`Examples.Todo.editTodo.blur.sound`
proved	sound cancel	`Examples.Todo.editTodo.cancel.sound`
fuzzed	Not shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).
tested	Not shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95).
seen	Not shown yet: a screenshot of the app shows it. A CI step will publish it (#95).

Where it's defined

Declaration: Examples.Todo.editTodo
Module: Todo
Source: lean/Todo.lean:114 at v0.2.0
Statement: Examples.Todo.editTodo.enabled Examples.Todo.editTodo.edit.post Examples.Todo.editTodo.submit.post Examples.Todo.editTodo.blur.post Examples.Todo.editTodo.cancel.post
Statement hash: 7896f5dd84b27f5a

Ledger

cairn_examples^207 is active in this version's claims.lock, statement 7896f5dd84b27f5a. An id never moves or changes meaning.