		Search-engine friendly clone of the ACL2 documentation.

Logand-defaults

Behavior of logand on bad inputs.

Definitions and Theorems

Theorem: logand-default-1

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

Theorem: logand-default-2

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