Edges are admitted when their peers are distinct, strictly ascending,
differ from this role, and every address is one IPv4 socket address.
307def nativePeerEdgesAdmitted =
308 (lambda unrestricted role : Nat .
309 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
310 (stdListFold
311 (family NativePeerEdge)
312 (pi unrestricted floor : Nat . Nat)
313 (lambda unrestricted edge : (family NativePeerEdge) .
314 (lambda unrestricted next : (pi unrestricted floor : Nat . Nat) .
315 (lambda unrestricted floor : Nat .
316 (naturalAnd
317 (naturalLessOrEqual floor (nativePeerEdgePeerOf edge))
318 (naturalAnd
319 (naturalIsZero (naturalEqual role (nativePeerEdgePeerOf edge)))
320 (naturalAnd
321 (naturalEqual
322 (bytes-length (nativePeerEdgeAddressOf edge))
323 linuxIPv4SocketAddressBytes)
324 (next (succ (nativePeerEdgePeerOf edge)))))))))
325 (lambda unrestricted floor : Nat . 1)
326 edges
327 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.