Posp
A recognizer for the positive integers
(posp x) is logically equivalent to (not (zp x)) (see
zp) and also to (and (natp x) (not (equal x 0))).
The community book arithmetic/natp-posp has some lightweight rules
for reasoning about posp and natp, and is included in the arithmetic-1 library. For a somewhat heavier and more comprehensive
alternative, you may wish to instead see the arith-equivs book.
Function: posp
(defun posp (x)
(declare (xargs :guard t))
(and (integerp x) (< 0 x)))
Subtopics
- Pos-fix
- (pos-fix x) is a fixing function for posp: it is the
identity for positive integers, or returns 1 for any other object.
- Pos-equiv
- (pos-equiv x y) is equality for positive numbers, i.e., equality up
to pos-fix.
- Lposfix
- (lposfix x) is logically identical to (pos-fix x), but its
guard requires that x is a posp and, in the execution, it's just a
no-op that returns x.
