@@ -122,12 +122,12 @@ public
122122bitsLShr : Bits n -> Bits n -> Bits n
123123bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)
124124
125−bitsAShr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
125+bitsAShr' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
126126bitsAShr' {n=n} x c with (log2Bytes n)
127− | O = prim__ashrB8 x c
128− | S O = prim__ashrB16 x c
129− | S (S O) = prim__ashrB32 x c
130− | S (S (S _)) = prim__ashrB64 x c
127+ | O = pad8' n prim__ashrB8 x c
128+ | S O = pad16' n prim__ashrB16 x c
129+ | S (S O) = pad32' n prim__ashrB32 x c
130+ | S (S (S _)) = pad64' n prim__ashrB64 x c
131131
132132public
133133bitsAShr : Bits n -> Bits n -> Bits n