Filtering...

defconst-fast

books/make-event/defconst-fast
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))))))