Descend from `node` toward `target`, at most `fuel` edges. Fan-out of at
least two bounds the depth by log2 of the count, so 64 levels cover every
role a 64-bit count names; a chain (fan-out one) needs fuel = count.
159def participantTreeDescend =
160 (lambda unrestricted fanout : Nat .
161 (lambda unrestricted fuel : Nat .
162 (nat-eliminate
163 (lambda unrestricted remaining : Nat .
164 (pi unrestricted node : (family ParticipantTreeNode) .
165 (pi unrestricted target : Nat . (family ParticipantTreeNode))))
166 (lambda unrestricted node : (family ParticipantTreeNode) .
167 (lambda unrestricted target : Nat . node))
168 (lambda unrestricted previous : Nat .
169 (lambda unrestricted deeper : (pi unrestricted node : (family ParticipantTreeNode) . (pi unrestricted target : Nat . (family ParticipantTreeNode))) .
170 (lambda unrestricted node : (family ParticipantTreeNode) .
171 (lambda unrestricted target : Nat .
172 (nat-eliminate
173 (lambda unrestricted found : Nat . (family ParticipantTreeNode))
174 (deeper
175 (participantTreeChildNode
176 fanout
177 node
178 (participantTreeChildHolding fanout node target))
179 target)
180 (lambda unrestricted predecessor : Nat .
181 (lambda unrestricted ignored : (family ParticipantTreeNode) . node))
182 (naturalEqual (participantTreeRoleOf node) target))))))
183 fuel)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.