		Search-engine friendly clone of the ACL2 documentation.

Defsoft-implementation

Defsoft-macro-definition

Definition of the defsoft macro.

Macro: defsoft

(defmacro defsoft (fn)
 (cons
  'with-output
  (cons
   ':gag-mode
   (cons
    'nil
    (cons
     ':off
     (cons
      (set-difference-eq acl2::*valid-output-names*
                         '(error observation))
      (cons
       ':stack
       (cons
        ':push
        (cons
         (cons
          'make-event
          (cons
           (cons
            'defsoft-fn
            (cons
                (cons 'quote (cons fn 'nil))
                (cons (cons 'cons
                            (cons ''defsoft
                                  (cons (cons 'quote (cons fn 'nil))
                                        'nil)))
                      '(state))))
           '(:on-behalf-of :quiet!)))
         'nil)))))))))

Macro: defsoft

(defmacro acl2::defsoft (&rest args)
  (cons 'defsoft args))