A star of `owners` admits owner 0 with one address per other owner and
every other owner with exactly one address, all admitted edges.
357def nativePeerStarAdmitted =
358 (lambda unrestricted owners : Nat .
359 (lambda unrestricted role : Nat .
360 (lambda unrestricted addresses : (family StdList Bytes) .
361 (naturalAnd
362 (naturalLess role owners)
363 (naturalAnd
364 (naturalEqual
365 (stdListLength Bytes addresses)
366 (naturalSelect (naturalIsZero role) (naturalPredecessor owners) 1))
367 (nativePeerEdgesAdmitted role (nativePeerStarEdges role addresses)))))))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.