other
(in-package "ACL2")
defconst-fastmacro
(defmacro defconst-fast (name form &optional (doc '"" doc-p)) `(make-event (let ((val ,FORM)) (list* 'defconst ',NAME (list 'quote val) ,(AND DOC-P (LIST 'LIST DOC))))))
(in-package "ACL2")
(defmacro defconst-fast (name form &optional (doc '"" doc-p)) `(make-event (let ((val ,FORM)) (list* 'defconst ',NAME (list 'quote val) ,(AND DOC-P (LIST 'LIST DOC))))))