23 lines
698 B
Plaintext
23 lines
698 B
Plaintext
(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)))
|