Expand description
A plan node’s address: the dotted path that says where it hangs.
The part crates/kernel/spec/NodeId.lean specifies this module.
A value, and that is why it is not in kernel::plan. The tree
decides — what may be started, what a branch is worth, which of the
two exits a held node takes. This only says what a well-formed
address is, and refuses everything else at the one construction
point, so nothing downstream has to ask again. plan is shape 1;
this is shape 2 (ARCHITECTURE.md section 9).
The hand-written Deserialize is the load-bearing part. A derived
one would accept any string off the wire and hand back a NodeId
that never passed parse, which is the whole of what this type is
for.
Structs§
- NodeId
- A node’s place in the plan, as the first column spells it:
2,2.3,2.3.1. The parent is the prefix, so the tree needs no second field to say where a node hangs.
Constants§
- NODE_
DEPTH_ MAX - The longest branch a plan may grow. Ten levels of
1.1.1.…is a depth no plan has ever needed and a length past which the index column stops being readable; refusing it also bounds every walk in this module.