Expand description
Repair leases: when the environment itself is
broken, repair is serialized — one live lease per scope subtree, so
two runs can never “fix” the same breakage into a bigger one. The
active table is the caller’s state; kernel only judges.
The part crates/kernel/spec/Repair.lean specifies this module.
Enums§
- Repair
Verdict - Deliberately exhaustive verdict. Queued is a legal outcome, not an error — E_REPAIR_BUSY only carries it across the tool surface.
Functions§
- request
- Overlap either way queues (same rule as goal resources); the same holder re-requesting its exact scope re-leases (idempotent recovery). First overlapping holder wins the report, in BTreeMap order.