Expand description
Completion and progress. Claiming done makes
nothing done: Completion::Done cannot be built without evidence the
city recorded itself (the runtime checks depth). Progress
is honest in the type: only a planned run owns a ratio method —
an unplanned run has nothing to ask a percentage from.
The part crates/kernel/spec/Completion.lean specifies this module.
Structs§
- Evidence
- Non-empty, and every ref kind is in
CITABLE. There is no other constructor and no Deserialize anywhere in the chain — history cannot be claimed, only cited. - Planned
Progress - Progress with a denominator: the leaves of the plan tree.
- Unplanned
Progress - Progress without a denominator: steps walked and budget burned. No ratio method exists — the interface cannot paint what it cannot know (A17’s type half).
Enums§
- Completion
- The three endings; a fourth cannot be represented (frozen surface,
14.1).
Limitis not a kind of done — record limit, not completion. - Progress
- Deliberately exhaustive: both faces must be handled by every renderer.