231def participantCompileRepeat =
232 (lambda unrestricted count : Nat .
233 (lambda unrestricted stride : Nat .
234 (lambda unrestricted inner : (family ParticipantIndex) .
235 (participantRequire
236 (family ParticipantIndex)
237 (naturalNonzero count)
238 (constructor ParticipantGroupFailure ParticipantEmptySelection)
239 (participantRequire
240 (family ParticipantIndex)
241 (naturalAnd
242 (naturalLessOrEqual stride participantWordLimit)
243 (naturalLess
244 (naturalSaturatingSubtract (participantUpperOf inner) (participantLowerOf inner))
245 stride))
246 (constructor ParticipantGroupFailure ParticipantRepeatedOverlap)
247 (let unrestricted last =
248 (naturalAdd
249 (participantUpperOf inner)
250 (naturalMultiply (naturalSaturatingSubtract count 1) stride))
251 in
252 (let unrestricted size =
253 (naturalMultiply count (participantCountOf inner))
254 in
255 (participantRequire
256 (family ParticipantIndex)
257 (naturalAnd
258 (naturalLessOrEqual last participantWordLimit)
259 (naturalLessOrEqual size participantWordLimit))
260 (constructor ParticipantGroupFailure ParticipantCoordinateOverflow)
261 (constructor
262 StdResult
263 StdSuccess
264 (family ParticipantGroupFailure)
265 (family ParticipantIndex)
266 (constructor
267 ParticipantIndex
268 ParticipantRepeatIndex
269 (constructor
270 ParticipantBounds
271 ParticipantBoundsOf
272 (participantLowerOf inner)
273 last
274 size
275 (naturalAdd 1 (participantNodesOf inner))
276 (naturalAdd 1 (participantDepthOf inner)))
277 stride
278 inner))))))))))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.