(defun symbol-to-constant (sym)
   (intern (concatenate 'string "*" (symbol-name sym) "*")
           "ACL2"))

(defmacro enum-with-vals (symbol value &rest args)
   (if (endp args)
       `(defconst ,(symbol-to-constant symbol) ,value)
       `(progn (defconst ,(symbol-to-constant symbol) ,value)
               (enum-with-vals ,@args))))

(defun interleave-with-nats-r (xs i)
   (if (endp xs)
       nil
       (cons (first xs)
             (cons i (interleave-with-nats-r (rest xs)
                                             (1+ i))))))

(defun interleave-with-nats (xs)
   (interleave-with-nats-r xs 0))

(defmacro enum (&rest symbols)
   `(enum-with-vals ,@(interleave-with-nats symbols)))