		Search-engine friendly clone of the ACL2 documentation.

Primitive-function-macros

Def-double-binary

Specialization of def-primitive-binary to the case in which input and output types are double.

Macro: def-double-binary

(defmacro def-double-binary
          (name &key
                operation commutative commutative-hints
                (parents 'nil parents-suppliedp)
                (short 'nil short-suppliedp)
                (long 'nil long-suppliedp))
 (cons
  'def-primitive-binary
  (cons
   name
   (cons
    ':in-type-left
    (cons
     '(primitive-type-double)
     (cons
      ':in-type-right
      (cons
       '(primitive-type-double)
       (cons
        ':out-type
        (cons
         '(primitive-type-double)
         (cons
          ':operation
          (cons
           operation
           (cons
            ':commutative
            (cons
             commutative
             (cons
              ':commutative-hints
              (cons
               commutative-hints
               (append
                   (and parents-suppliedp
                        (list :parents parents))
                   (append (and short-suppliedp (list :short short))
                           (and long-suppliedp
                                (list :long long)))))))))))))))))))