cairn_examples^205 Edit a todo

What you do

Double-click a todo's title. (T20, T25–T27)

What you see

The todo's row becomes a field holding its title, with the caret at the end and keyboard focus in it; any other todo in edit mode is replaced. Nothing else changes.

Evidence

proved	sound doublePress	`Examples.Todo.startEditing.doublePress.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.startEditing
Module: Todo
Source: lean/Todo.lean:86 at v0.2.0
Statement: Examples.Todo.startEditing.enabled Examples.Todo.startEditing.doublePress.post
Statement hash: 2943b794f7d59288

Ledger

cairn_examples^205 is active in this version's claims.lock, statement 2943b794f7d59288. An id never moves or changes meaning.