The connection slot of the edge to `peer`, or the scratch slot (which no
edge owns) when the participant has no such edge; admission of the caller's
topology must refuse that case before commands are generated.
288def nativePeerEdgeConnectionTo =
289 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
290 (lambda unrestricted peer : Nat .
291 (stdListFold
292 (family NativePeerEdge)
293 (pi unrestricted index : Nat . Nat)
294 (lambda unrestricted edge : (family NativePeerEdge) .
295 (lambda unrestricted next : (pi unrestricted index : Nat . Nat) .
296 (lambda unrestricted index : Nat .
297 (naturalSelect
298 (naturalEqual (nativePeerEdgePeerOf edge) peer)
299 (nativePeerEdgeConnectionSlot index)
300 (next (succ index))))))
301 (lambda unrestricted index : Nat . nativePeerScratchSlot)
302 edges
303 0)))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.