hons-help2

other

(in-package "ACL2")

include-book

(include-book "hons-help")

def-macro-aliasmacro

(defmacro def-macro-alias
  (mac fn arity-or-args)
  (let ((args (if (integerp arity-or-args)
         (make-var-lst 'x arity-or-args)
         arity-or-args)))
    `(progn (defmacro ,MAC
        ,ARGS
        (list ',FN ,@(REMOVE1-EQ '&OPTIONAL ARGS)))
      (add-macro-alias ,MAC ,FN))))

other

(def-macro-alias hqual hons-equal 2)

other

(def-macro-alias hopy hons-copy 1)

other

(def-macro-alias assoc-hqual hons-assoc-equal 2)

other

(def-macro-alias het hons-get (x a))

other

(def-macro-alias hut hons-acons 3)

other

(def-macro-alias hshrink-alist hons-shrink-alist 2)

histmacro

(defmacro hist (&rest x) `(hons-list ,@X))

hist*macro

(defmacro hist* (&rest x) `(hons-list* ,@X))

Included Books