The fixed24 payload is exactly three bytes. Reuse the qualified low-to-high
bit writer; preserve neighboring bits and one-field24-bit telemetry.
496def sm86PlaceWord24BitsUnchecked =
497 (lambda unrestricted position : Nat .
498 (lambda unrestricted byte0 : Byte .
499 (lambda unrestricted byte1 : Byte .
500 (lambda unrestricted byte2 : Byte .
501 (lambda unrestricted encoded : Bytes .
502 (sm86PlaceFieldBitsUnchecked
503 (naturalAdd position (byte-to-nat (byte 16)))
504 (byte-to-nat (byte 8))
505 (byte-to-nat byte2)
506 (sm86PlaceFieldBitsUnchecked
507 (naturalAdd position (byte-to-nat (byte 8)))
508 (byte-to-nat (byte 8))
509 (byte-to-nat byte1)
510 (sm86PlaceFieldBitsUnchecked
511 position
512 (byte-to-nat (byte 8))
513 (byte-to-nat byte0)
514 encoded))))))))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.