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.