		Search-engine friendly clone of the ACL2 documentation.

Floating-point-macro-placeholders

Def-primitive-binary-abs

Macro to introduce an abstract placeholder for a binary operation or a conversion involving floating-point values.

Macro: def-primitive-binary-abs

(defmacro def-primitive-binary-abs (name type)
  (cons 'make-event
        (cons (cons 'def-primitive-binary-abs-fn
                    (cons (cons 'quote (cons name 'nil))
                          (cons type 'nil)))
              'nil)))

Definitions and Theorems

Function: def-primitive-binary-abs-fn

(defun def-primitive-binary-abs-fn (name type)
 (declare (xargs :guard (and (symbolp name)
                             (primitive-typep type))))
 (let ((__function__ 'def-primitive-binary-abs-fn))
  (declare (ignorable __function__))
  (b* ((result (def-primitive-unary/binary-abs-term type))
       (predicate (def-primitive-unary/binary-abs-predicate type))
       (thm-name (add-suffix name "-TYPE")))
   (cons
    'encapsulate
    (cons
     (cons (cons (cons name '(* *)) '(=> *))
           'nil)
     (cons
       (cons 'local
             (cons (cons 'defun
                         (cons name
                               (cons '(x y)
                                     (cons '(declare (ignore x y))
                                           (cons result 'nil)))))
                   'nil))
       (cons (cons 'defthm
                   (cons thm-name
                         (cons (cons predicate
                                     (cons (cons name '(x y)) 'nil))
                               'nil)))
             'nil)))))))