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 c 0 bits if c is positive, shifting right and
dropping (abs c) bits if c is negative, and simply returning i if c
is 0.
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.
