The nodes from the root down to (excluding) `role`'s node: the ancestors
a participant consults to verify that its own subtree is part of one
published root, in root-first order. At most the hierarchy's height.
247def participantTreeAncestors =
248 (lambda unrestricted fanout : Nat .
249 (lambda unrestricted count : Nat .
250 (lambda unrestricted role : Nat .
251 (app
252 (nat-eliminate
253 (lambda unrestricted remaining : Nat .
254 (pi unrestricted node : (family ParticipantTreeNode) .
255 (family StdList (family ParticipantTreeNode))))
256 (lambda unrestricted node : (family ParticipantTreeNode) .
257 (constructor StdList StdListEmpty (family ParticipantTreeNode)))
258 (lambda unrestricted previous : Nat .
259 (lambda unrestricted deeper : (pi unrestricted node : (family ParticipantTreeNode) . (family StdList (family ParticipantTreeNode))) .
260 (lambda unrestricted node : (family ParticipantTreeNode) .
261 (nat-eliminate
262 (lambda unrestricted found : Nat .
263 (family StdList (family ParticipantTreeNode)))
264 (constructor
265 StdList
266 StdListCons
267 (family ParticipantTreeNode)
268 node
269 (deeper
270 (participantTreeChildNode
271 fanout
272 node
273 (participantTreeChildHolding fanout node role))))
274 (lambda unrestricted predecessor : Nat .
275 (lambda unrestricted ignored : (family StdList (family ParticipantTreeNode)) .
276 (constructor StdList StdListEmpty (family ParticipantTreeNode))))
277 (naturalEqual (participantTreeRoleOf node) role)))))
278 (participantTreeFuel fanout count))
279 (participantTreeRoot count)))))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.