Project one role from a regular partition in constant arithmetic work.
The quotient/remainder law keeps every endpoint <= extent; intermediate
multiplication cannot overflow for an admitted role and U64 extent.
No list of 200,000 ranks and no recursion on an integer magnitude is built.
103def balancedIntervalUnchecked =
104 (lambda unrestricted extent : Nat .
105 (lambda unrestricted participants : Nat .
106 (lambda unrestricted role : Nat .
107 (app
108 (lambda unrestricted quotient : Nat .
109 (app
110 (lambda unrestricted remainder : Nat .
111 (app
112 (lambda unrestricted begin : Nat .
113 (constructor
114 LogicalInterval
115 LogicalIntervalOf
116 begin
117 (naturalAdd begin (naturalAdd quotient (naturalLess role remainder)))))
118 (naturalAdd (naturalMultiply quotient role) (naturalMinimum role remainder))))
119 (naturalModuloUnchecked extent participants)))
120 (naturalDivideUnchecked extent participants)))))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.