SIGNED division through magnitudes: |a| / |b| unsigned, then the quotient
is negated when the signs differ and the remainder when the dividend is
negative. |signedMinimum| = 2^(width-1) is representable unsigned, so the
wrapping API needs no special case: 2^(width-1) / 1 negated wraps back to
signedMinimum with remainder 0. The checked API refuses exactly that shape.
1501def stdU64NegateIf =
1502 (lambda unrestricted flag : Nat .
1503 (lambda unrestricted bits : (family ModelWord64) .
1504 (modelWord64Select flag (modelWord64Subtract modelWord64Zero bits) bits)))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.