A 19-bit branch field at bit 5, with `extra` in byte 0 (a condition or a register).
829def aarch64Branch19Word =
830 (lambda unrestricted base3 : Nat .
831 (lambda unrestricted extra : Nat .
832 (lambda unrestricted direction : (family AArch64Direction) .
833 (lambda unrestricted distance : Nat .
834 (nat-eliminate
835 (lambda unrestricted aligned : Nat . (family AArch64EncodeResult))
836 (constructor AArch64EncodeResult AArch64MisalignedOffset distance)
837 (lambda unrestricted predecessorAligned : Nat .
838 (lambda unrestricted inductionAligned : (family AArch64EncodeResult) .
839 (nat-eliminate
840 (lambda unrestricted accepted : Nat . (family AArch64EncodeResult))
841 (constructor AArch64EncodeResult AArch64DisplacementOutOfRange distance)
842 (lambda unrestricted predecessor : Nat .
843 (lambda unrestricted induction : (family AArch64EncodeResult) .
844 (app
845 (lambda unrestricted field : Nat .
846 (aarch64ByteWord
847 (naturalAdd extra (aarch64FromBitFiveByte0 field))
848 (aarch64FromBitFiveByte1 field)
849 (aarch64FromBitFiveByte2 field)
850 base3))
851 (aarch64SignedField
852 direction
853 (naturalDivideUnchecked distance aarch64Four)
854 aarch64Modulus19))))
855 (aarch64DistanceAccepted
856 direction
857 (naturalDivideUnchecked distance aarch64Four)
858 (naturalDivideUnchecked aarch64Modulus19 aarch64Two)))))
859 (naturalIsZero (naturalModuloUnchecked distance aarch64Four)))))))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.