Each hex digit shifts four bits once; six digits fit in the 24 low bits.
504def quotedAppendHexDigit =
505 (lambda unrestricted word : (family ModelWord32) .
506 (lambda unrestricted digit : Nat .
507 (eliminate
508 ModelWord32
509 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
510 word
511 (branch
512 ModelWord32Value
513 b0
514 b1
515 b2
516 b3
517 .
518 (constructor
519 ModelWord32
520 ModelWord32Value
521 (nat-to-byte
522 (Std.Natural/naturalAdd
523 (byte-to-nat (Std.Byte/byteShiftLeftTruncated b0 (byte-to-nat (byte 4))))
524 digit))
525 (Std.Byte/byteOr
526 (Std.Byte/byteShiftLeftTruncated b1 (byte-to-nat (byte 4)))
527 (Std.Byte/byteShiftRight b0 (byte-to-nat (byte 4))))
528 (Std.Byte/byteOr
529 (Std.Byte/byteShiftLeftTruncated b2 (byte-to-nat (byte 4)))
530 (Std.Byte/byteShiftRight b1 (byte-to-nat (byte 4))))
531 (Std.Byte/byteOr
532 (Std.Byte/byteShiftLeftTruncated b3 (byte-to-nat (byte 4)))
533 (Std.Byte/byteShiftRight b2 (byte-to-nat (byte 4)))))))))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.