The role's edges with addresses listed in the hierarchy's edge order
(parent first unless root, then children in role order): the form a
caller that compiles each role's own addresses supplies.
73def nativePeerTreeEdgesListed =
74 (lambda unrestricted fanout : Nat .
75 (lambda unrestricted owners : Nat .
76 (lambda unrestricted role : Nat .
77 (lambda unrestricted addresses : (family StdList Bytes) .
78 (stdListFold
79 (family NativePeerEdge)
80 (pi unrestricted index : Nat . (family StdList (family NativePeerEdge)))
81 (lambda unrestricted edge : (family NativePeerEdge) .
82 (lambda unrestricted next : (pi unrestricted index : Nat . (family StdList (family NativePeerEdge))) .
83 (lambda unrestricted index : Nat .
84 (constructor
85 StdList
86 StdListCons
87 (family NativePeerEdge)
88 (constructor
89 NativePeerEdge
90 NativePeerEdgeOf
91 (nativePeerEdgePeerOf edge)
92 (stdListHeadOr Bytes b"" (stdListDrop Bytes index addresses)))
93 (next (succ index))))))
94 (lambda unrestricted index : Nat .
95 (constructor StdList StdListEmpty (family NativePeerEdge)))
96 (nativePeerTreeEdges fanout owners role (lambda unrestricted child : Nat . b""))
97 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.