CONVERSIONS (L11l, NUM-005): sign-extension and narrowing are byte assembly,
never a round trip through Natural (which would be unary).
the byte that extends a sign: 0xff for negative, 0x00 for non-negative
591def stdI8SignByte =
592 (lambda unrestricted value : (family StdI8) .
593 (nat-eliminate
594 (lambda unrestricted current : Nat . Byte)
595 (byte 255)
596 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Byte . (byte 0)))
597 (stdI8IsNonNegative value)))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.