		Search-engine friendly clone of the ACL2 documentation.

Floating-point-macro-placeholders

Def-primitive-unary/binary-abs-predicate

Predicate for the result of a function introduced via def-primitive-unary-abs or def-primitive-binary-abs.

Signature
(def-primitive-unary/binary-abs-predicate type) → predicate
Arguments: type — Guard (primitive-typep type).
Returns: predicate — Type (symbolp predicate).

Definitions and Theorems

Function: def-primitive-unary/binary-abs-predicate

(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: symbolp-of-def-primitive-unary/binary-abs-predicate

(defthm symbolp-of-def-primitive-unary/binary-abs-predicate
  (b* ((predicate (def-primitive-unary/binary-abs-predicate type)))
    (symbolp predicate))
  :rule-classes :rewrite)

Theorem: def-primitive-unary/binary-abs-predicate-of-primitive-type-fix-type

(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: def-primitive-unary/binary-abs-predicate-primitive-type-equiv-congruence-on-type

(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)