		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-implementation

Defarbrec-macro-definition

Definition of the defarbrec macro.

Submit the event form generated by defarbrec-fn.

Macro: defarbrec

(defmacro defarbrec (&whole call fn x1...xn body &key update-names
                            terminates-name measure-name
                            (nonterminating ':nonterminating)
                            (print ':result)
                            show-only)
 (cons
  'make-event-terse
  (cons
   (cons
    'defarbrec-fn
    (cons
     (cons 'quote (cons fn 'nil))
     (cons
      (cons 'quote (cons x1...xn 'nil))
      (cons
       (cons 'quote (cons body 'nil))
       (cons
        (cons 'quote (cons update-names 'nil))
        (cons
         (cons 'quote
               (cons terminates-name 'nil))
         (cons
          (cons 'quote (cons measure-name 'nil))
          (cons
           (cons 'quote (cons nonterminating 'nil))
           (cons
            (cons 'quote (cons print 'nil))
            (cons
             (cons 'quote (cons show-only 'nil))
             (cons
                (cons 'quote (cons call 'nil))
                (cons (cons 'cons
                            (cons ''defarbrec
                                  (cons (cons 'quote (cons fn 'nil))
                                        'nil)))
                      '(state)))))))))))))
   (cons ':suppress-errors
         (cons (not print) 'nil)))))