		Search-engine friendly clone of the ACL2 documentation.

Defun2-implementation

Implementation of defun2.

Macro: defun2

(defmacro defun2 (sofun &rest rest)
  (list 'progn
        (list* 'defun sofun rest)
        (list 'defsoft sofun)))

Macro: defun2

(defmacro acl2::defun2 (&rest args)
  (list* 'defun2 args))