		Search-engine friendly clone of the ACL2 documentation.

Define2-implementation

Implementation of define2.

Macro: define2

(defmacro define2 (sofun &rest rest)
  (list 'progn
        (list* 'define sofun rest)
        (list 'defsoft sofun)))

Macro: define2

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