702def sm86EncodeShiftRightImmediate =
703 (lambda unrestricted guard : (family SM86InstructionGuard) .
704 (lambda unrestricted destination : (family SM86Register) .
705 (lambda unrestricted source : (family SM86Register) .
706 (lambda unrestricted amount : Byte .
707 (lambda unrestricted control : (family SM86Control) .
708 (nat-eliminate
709 (lambda unrestricted amountInvalid : Nat . (family SM86InstructionEncodingResult))
710 (sm86EncodeInstructionFields
711 sm86OpcodeShiftRightImmediate
712 guard
713 control
714 (sm86InstructionPrependField
715 sm86InstructionNaturalSixteen
716 sm86InstructionNaturalEight
717 (sm86RegisterNatural destination)
718 (sm86InstructionPrependField
719 sm86InstructionNaturalTwentyFour
720 sm86InstructionNaturalEight
721 (byte-to-nat (byte 255))
722 (sm86InstructionPrependField
723 sm86InstructionNaturalThirtyTwo
724 sm86InstructionNaturalThirtyTwo
725 (byte-to-nat amount)
726 (sm86InstructionPrependField
727 sm86InstructionNaturalSixtyFour
728 sm86InstructionNaturalEight
729 (sm86RegisterNatural source)
730 (sm86InstructionOneWord24Field
731 sm86InstructionNaturalSeventyTwo
732 (byte 22)
733 (byte 1)
734 (byte 0)))))))
735 (lambda unrestricted invalidPredecessor : Nat .
736 (lambda unrestricted invalidInduction : (family SM86InstructionEncodingResult) .
737 (sm86InstructionUnsupported (byte-to-nat (byte 9)))))
738 (nat-less-than (byte-to-nat (byte 31)) (byte-to-nat amount))))))))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.