		Search-engine friendly clone of the ACL2 documentation.

Ash

Arithmetic shift operation

(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.

Function: ash

(defun ash (i c)
  (declare (xargs :guard (and (integerp i) (integerp c))))
  (floor (* (ifix i) (expt 2 c)) 1))

Subtopics

Self-bounds-for-ash: Lemmas for the bounds of (ash a b) versus a.
Monotonicity-properties-of-ash: Lemmas about (ash a b) versus (ash a c).
Ihs/ash-lemmas: Lemmas about ash from the logops-lemmas book.
Ash-defaults: Behavior of ash on bad inputs.
Ash*: Recursive definition of ash.
(= 0 (ash 1 x))