Major Section: ACL2-BUILT-INS
(ash i c) is the result of taking the two's complement
representation of the integer
i and shifting it by
c bits: shifting
left and padding with
0 bits if
c is positive, shifting right and
(abs c) bits if
c is negative, and simply returning
The guard for
ash requires that its arguments are integers.
Ash is a Common Lisp function. See any Common Lisp documentation
for more information.
To see the ACL2 definition of this function, see pf.