		Search-engine friendly clone of the ACL2 documentation.

Floating-point-macro-placeholders

Def-primitive-unary/binary-abs-term

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

Signature
(def-primitive-unary/binary-abs-term type) → result
Arguments: type — Guard (primitive-typep type).
Returns: result — An untranslated term.

Definitions and Theorems

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

(defun def-primitive-unary/binary-abs-term (type)
  (declare (xargs :guard (primitive-typep type)))
  (let ((__function__ 'def-primitive-unary/binary-abs-term))
    (declare (ignorable __function__))
    (primitive-type-case type
                         :boolean nil
                         :char 0
                         :byte 0
                         :short 0
                         :int 0
                         :long 0
                         :float '(float-value-abs-pos-zero)
                         :double '(double-value-abs-pos-zero))))

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

(defthm
     def-primitive-unary/binary-abs-term-of-primitive-type-fix-type
 (equal
     (def-primitive-unary/binary-abs-term (primitive-type-fix type))
     (def-primitive-unary/binary-abs-term type)))

Theorem: def-primitive-unary/binary-abs-term-primitive-type-equiv-congruence-on-type

(defthm
 def-primitive-unary/binary-abs-term-primitive-type-equiv-congruence-on-type
 (implies (primitive-type-equiv type type-equiv)
          (equal (def-primitive-unary/binary-abs-term type)
                 (def-primitive-unary/binary-abs-term type-equiv)))
 :rule-classes :congruence)