18def cyclicRecordOffset = (lambda unrestricted completed : Nat . (lambda unrestricted iteration : Nat .
19 (lambda unrestricted count : Nat . (lambda unrestricted extent : Nat . (lambda unrestricted within : Nat .
20 (eliminate StdBool (lambda unrestricted current : (family StdBool) . (family CyclicRecordOffset))
21 (stdBoolFromNatural (naturalAnd (naturalLess 0 count)
22 (naturalAnd (naturalLess 0 extent) (naturalAnd (naturalLess within extent)
23 (naturalAnd (naturalLessOrEqual (naturalAdd completed iteration) cyclicRecordWordMaximum)
24 (naturalLessOrEqual (naturalMultiply count extent) cyclicRecordFileMaximum))))))
25 (branch StdTrue . (constructor CyclicRecordOffset CyclicRecordOffsetAccepted
26 (naturalAdd within (naturalMultiply extent (naturalModuloUnchecked (naturalAdd completed iteration) count)))))
27 (branch StdFalse . (constructor CyclicRecordOffset CyclicRecordOffsetRejected))))))))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.