The index of the child whose range holds `target` (a descendant of node).
134def participantTreeChildHolding =
135 (lambda unrestricted fanout : Nat .
136 (lambda unrestricted node : (family ParticipantTreeNode) .
137 (lambda unrestricted target : Nat .
138 (stdListFold
139 Nat
140 Nat
141 (lambda unrestricted index : Nat .
142 (lambda unrestricted rest : Nat .
143 (naturalSelect
144 (naturalLess
145 target
146 (participantTreeChildStart
147 fanout
148 (participantTreeRoleOf node)
149 (participantTreeSizeOf node)
150 (succ index)))
151 index
152 rest)))
153 0
154 (stdListNaturalsBelow (participantTreeChildCount fanout (participantTreeSizeOf node)))))))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.