Cairn
Docs
Claims
Blog
Packages
Claim · cairn_examples 0.2.0
cairn_examples^201 Todos window
A place of cairn_examples 0.2.0.
- Id
cairn_examples^201- Kind
- place
- Reads as
- no proof
- Version
- 0.2.0
What it is
The window: the heading, toggle all and the new-todo field, the listed todos, the footer with the counter, filters and Clear completed, and the info line.
In this place
Moves
| Id | Claim | Reads as |
|---|---|---|
cairn_examples^202 | New todoType in the What needs to be done? field, and press Enter. (T5–T13) | proved |
cairn_examples^203 | Mark all as completePress the toggle-all checkbox. (T14–T17) | proved |
cairn_examples^204 | Complete a todoPress a todo's checkbox. (T19, T42) | proved |
cairn_examples^205 | Edit a todoDouble-click a todo's title. (T20, T25–T27) | proved |
cairn_examples^206 | Delete a todoPress a todo's delete button (×, drawn while the pointer is over the row or the button has keyboard focus). (T21, T22, T49) | proved |
cairn_examples^207 | Edit fieldIn edit mode, type in the todo's field; then press Enter, click elsewhere or Tab away, or press Escape. (T28–T31, T50) | proved |
cairn_examples^208 | AllPress the All filter. (T39–T43) | proved |
cairn_examples^209 | ActivePress the Active filter. (T39–T43) | proved |
cairn_examples^210 | CompletedPress the Completed filter. (T39–T43) | proved |
cairn_examples^211 | Clear completedPress Clear completed, shown while some todo is completed. (T37, T38) | proved |
Flows
| Id | Claim | Reads as |
|---|---|---|
cairn_examples^216 | Add two todos and complete oneType milk and press Enter, type eggs with spaces around it and press Enter, then check milk. | proved |
cairn_examples^217 | Blank text adds nothingType spaces and press Enter. | proved |
cairn_examples^218 | Edit a todo and save with EnterAdd milk, double-click it, select all, type oat milk with spaces around it, press Enter. | proved |
cairn_examples^219 | Saving a blank edit deletes the todoAdd milk, double-click it, delete its text, and click elsewhere. | proved |
cairn_examples^220 | Escape cancels an editAdd milk, double-click it, delete its text, press Escape. | proved |
cairn_examples^221 | The Active filter hides completed todosAdd milk and eggs, check milk, press Active. | proved |
cairn_examples^222 | Clear completedAdd milk and eggs, check milk, press Clear completed. | proved |
cairn_examples^223 | Mark all as complete, then undo itAdd milk and eggs, check milk, press toggle all twice. | proved |
cairn_examples^224 | A new todo under the Completed filterAdd milk, press Completed, add eggs. | proved |
Evidence
| no proof | A place states where claims live; it has nothing to prove. | |
| 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.window- Module
Todo- Source
lean/Todo.lean:44atv0.2.0- Statement hash
-
Ledger
cairn_examples^201 is active in this version's claims.lock. An id never moves or changes meaning.