		Search-engine friendly clone of the ACL2 documentation.

Logior-defaults

Behavior of logior on bad inputs.

Definitions and Theorems

Theorem: logior-default-1

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

Theorem: logior-default-2

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