		Search-engine friendly clone of the ACL2 documentation.

Defunit-implementation

Defunit-macro-definition

Definition of the defunit macro.

Macro: defunit

(defmacro defunit (type &key
                        value pred fix equiv parents short long)
 (cons
  'make-event
  (cons
   (cons
    'defunit-fn
    (cons
     (cons 'quote (cons type 'nil))
     (cons
        (cons 'quote (cons value 'nil))
        (cons (cons 'quote (cons pred 'nil))
              (cons (cons 'quote (cons fix 'nil))
                    (cons (cons 'quote (cons equiv 'nil))
                          (cons (cons 'quote (cons parents 'nil))
                                (cons short (cons long 'nil)))))))))
   'nil)))