A wait interval is valid when it is at least one nanosecond and below one
second (999,999,999 nanoseconds), so a timespec with a zero seconds field
carries it.
583def nativePhysicalFenceWaitIntervalValid =
584 (lambda unrestricted interval : (family ModelWord64) .
585 (naturalAnd
586 (naturalIsZero (modelWord64IsZero interval))
587 (modelWord64LessThan interval (modelWord64FromNaturalTruncated 1000000000))))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.