Arithmetic shift, unsigned version.
(ashu size i cnt) → nat
- size — Guard (and (integerp size) (< 0 size)).
- i — Guard (integerp i).
- cnt — Guard (integerp cnt).
- nat — Type (natp nat).
ashu is a fixed-width version of ash. The integer
i is first coerced to a size-bit signed integer by sign-extension,
then shifted with ash, and finally truncated back to a size-bit
See also lshu for a logical (instead of arithmetic) shift.
Definitions and Theorems
(defun ashu (size i cnt)
(declare (xargs :guard (and (and (integerp size) (< 0 size))
(let ((__function__ 'ashu))
(declare (ignorable __function__))
(loghead size (ash (logext size i) cnt))))
(b* ((nat (ashu size i cnt)))