cairn_examples^202 New todo

What you do

Type in the What needs to be done? field, and press Enter. (T5–T13)

What you see

The text appears in the field. Enter adds the trimmed text as an active todo at the end of the list and clears the field; blank text adds nothing and stays in the field. Nothing else changes.

Evidence

proved	sound edit	`Examples.Todo.newTodo.edit.sound`
proved	sound submit	`Examples.Todo.newTodo.submit.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.newTodo
Module: Todo
Source: lean/Todo.lean:47 at v0.2.0
Statement: Examples.Todo.newTodo.edit.post Examples.Todo.newTodo.submit.post
Statement hash: 20a9247beb8fd04e

Ledger

cairn_examples^202 is active in this version's claims.lock, statement 20a9247beb8fd04e. An id never moves or changes meaning.