Predicate for the result of a function introduced via def-primitive-unary-abs or def-primitive-binary-abs.
(def-primitive-unary/binary-abs-predicate type) → predicate
Function:
(defun def-primitive-unary/binary-abs-predicate (type) (declare (xargs :guard (primitive-typep type))) (let ((__function__ 'def-primitive-unary/binary-abs-predicate)) (declare (ignorable __function__)) (primitive-type-case type :boolean 'booleanp :char 'ubyte16p :byte 'sbyte8p :short 'sbyte16p :int 'sbyte32p :long 'sbyte64p :float 'float-value-abs-p :double 'double-value-abs-p)))
Theorem:
(defthm symbolp-of-def-primitive-unary/binary-abs-predicate (b* ((predicate (def-primitive-unary/binary-abs-predicate type))) (symbolp predicate)) :rule-classes :rewrite)
Theorem:
(defthm def-primitive-unary/binary-abs-predicate-of-primitive-type-fix-type (equal (def-primitive-unary/binary-abs-predicate (primitive-type-fix type)) (def-primitive-unary/binary-abs-predicate type)))
Theorem:
(defthm def-primitive-unary/binary-abs-predicate-primitive-type-equiv-congruence-on-type (implies (primitive-type-equiv type type-equiv) (equal (def-primitive-unary/binary-abs-predicate type) (def-primitive-unary/binary-abs-predicate type-equiv))) :rule-classes :congruence)