An imm16 occupies bits 5-20, an imm19 bits 5-23: both start at bit 5.
616def aarch64FromBitFiveByte0 =
617 (lambda unrestricted value : Nat .
618 (naturalMultiply (naturalModuloUnchecked value aarch64Eight) aarch64ThirtyTwo))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.