199def participantCompileStride =
200 (lambda unrestricted first : Nat .
201 (lambda unrestricted stride : Nat .
202 (lambda unrestricted count : Nat .
203 (participantRequire
204 (family ParticipantIndex)
205 (naturalNonzero count)
206 (constructor ParticipantGroupFailure ParticipantEmptySelection)
207 (participantRequire
208 (family ParticipantIndex)
209 (naturalAnd (naturalNonzero stride) (naturalLessOrEqual stride participantWordLimit))
210 (constructor ParticipantGroupFailure ParticipantZeroStride)
211 (let unrestricted last =
212 (naturalAdd first (naturalMultiply (naturalSaturatingSubtract count 1) stride))
213 in
214 (participantRequire
215 (family ParticipantIndex)
216 (naturalAnd
217 (naturalLessOrEqual count participantWordLimit)
218 (naturalLessOrEqual last participantWordLimit))
219 (constructor ParticipantGroupFailure ParticipantCoordinateOverflow)
220 (constructor
221 StdResult
222 StdSuccess
223 (family ParticipantGroupFailure)
224 (family ParticipantIndex)
225 (constructor
226 ParticipantIndex
227 ParticipantStrideIndex
228 (constructor ParticipantBounds ParticipantBoundsOf first last count 1 1)
229 stride)))))))))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.