Negp
Recognizer for negative integers.
Definitions and Theorems
Function: negp
(defun negp (x)
(declare (xargs :guard t))
(and (integerp x) (< x 0)))
Theorem: negp-compound-recognizer
(defthm negp-compound-recognizer
(equal (negp x)
(and (integerp x) (< x 0)))
:rule-classes :compound-recognizer)
