		Search-engine friendly clone of the ACL2 documentation.

Ash-defaults

Behavior of ash on bad inputs.

Theorem: ash-default-1

(defthm ash-default-1
  (implies (not (integerp x))
           (equal (ash x y) 0))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: ash-default-2

(defthm ash-default-2
  (implies (not (integerp y))
           (equal (ash x y) (ifix x)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))