Term for the result of a function introduced via def-primitive-unary-abs or def-primitive-binary-abs.
(def-primitive-unary/binary-abs-term type) → result
Function:
(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:
(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:
(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)