---- who holds which words ----
The one-word intervals of the indices below `count` whose coordinate
(index mod k) this role owns.
108def dpotOwnedWords =
109 (lambda unrestricted k : Nat .
110 (lambda unrestricted owners : Nat .
111 (lambda unrestricted role : Nat .
112 (lambda unrestricted count : Nat .
113 (stdListFold
114 Nat
115 (family StdList (family LogicalInterval))
116 (lambda unrestricted index : Nat .
117 (lambda unrestricted rest : (family StdList (family LogicalInterval)) .
118 (nat-eliminate
119 (lambda unrestricted held : Nat . (family StdList (family LogicalInterval)))
120 rest
121 (lambda unrestricted previous : Nat .
122 (lambda unrestricted ignored : (family StdList (family LogicalInterval)) .
123 (constructor
124 StdList
125 StdListCons
126 (family LogicalInterval)
127 (dpoInterval (naturalMultiply dpWord index) dpWord)
128 rest)))
129 (dpoOwns owners role (naturalModuloUnchecked index k)))))
130 (constructor StdList StdListEmpty (family LogicalInterval))
131 (stdListNaturalsBelow count))))))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.