A fixed32 field keeps its already bounded four-byte representation.
Each reused bit loop sees one byte only; target positions may be unaligned.
407def sm86PlaceWord32BitsUnchecked =
408 (lambda unrestricted position : Nat .
409 (lambda unrestricted value : (family SM86Unsigned32) .
410 (lambda unrestricted encoded : Bytes .
411 (eliminate
412 SM86Unsigned32
413 (lambda unrestricted current : (family SM86Unsigned32) . Bytes)
414 value
415 (branch
416 SM86Unsigned32Value
417 byte0
418 byte1
419 byte2
420 byte3
421 .
422 (sm86PlaceFieldBitsUnchecked
423 (naturalAdd position (byte-to-nat (byte 24)))
424 sm86EncodingNaturalEight
425 (byte-to-nat byte3)
426 (sm86PlaceFieldBitsUnchecked
427 (naturalAdd position sm86EncodingNaturalSixteen)
428 sm86EncodingNaturalEight
429 (byte-to-nat byte2)
430 (sm86PlaceFieldBitsUnchecked
431 (naturalAdd position sm86EncodingNaturalEight)
432 sm86EncodingNaturalEight
433 (byte-to-nat byte1)
434 (sm86PlaceFieldBitsUnchecked
435 position
436 sm86EncodingNaturalEight
437 (byte-to-nat byte0)
438 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.