Cairn
Docs
Claims
Blog
Packages
Claim · cairn_examples 0.2.0
cairn_examples^206 Delete a todo
A move of cairn_examples 0.2.0, in Todos window.
- Id
cairn_examples^206- Kind
- move
- Reads as
- proved
- Place
- Todos window
^201 - Version
- 0.2.0
What you do
Press a todo's delete button (×, drawn while the pointer is over the row or the button has keyboard focus). (T21, T22, T49)
What you see
The todo is gone, with its row. Nothing else changes.
Evidence
| proved | sound press | Examples.Todo.deleteTodo.press.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.deleteTodo- Module
Todo- Source
lean/Todo.lean:99atv0.2.0- Statement
Examples.Todo.deleteTodo.enabledExamples.Todo.deleteTodo.press.post- Statement hash
6f4391a930943988
Ledger
cairn_examples^206 is active in this version's claims.lock, statement 6f4391a930943988. An id never moves or changes meaning.