AlphaGitHub
Source/Packages

Runtime.NativePeerEndpoint

packages/execution/src/Runtime/NativePeerEndpoint.alpha

405 lines36 declarations17.3 KiBSHA-256 3f09597de6f2
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 332–353

nativePeerStarEdges

Full file
A star centred on role 0: role 0 has an edge to every other role, in order, at `addresses`; every other role has one edge, to role 0, at its one address.
332def nativePeerStarEdges =
333  (lambda unrestricted role : Nat .
334    (lambda unrestricted addresses : (family StdList Bytes) .
335      (stdListFold
336        Bytes
337        (pi unrestricted index : Nat . (family StdList (family NativePeerEdge)))
338        (lambda unrestricted address : Bytes .
339          (lambda unrestricted next : (pi unrestricted index : Nat . (family StdList (family NativePeerEdge))) .
340            (lambda unrestricted index : Nat .
341              (constructor
342                StdList
343                StdListCons
344                (family NativePeerEdge)
345                (constructor
346                  NativePeerEdge
347                  NativePeerEdgeOf
348                  (naturalSelect (naturalIsZero role) (succ index) 0)
349                  address)
350                (next (succ index))))))
351        (lambda unrestricted index : Nat . (constructor StdList StdListEmpty (family NativePeerEdge)))
352        addresses
353        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.