		Search-engine friendly clone of the ACL2 documentation.

Sd-key-p

Make-honsed-sd-key

Constructor macro for honsed sd-key-p structures.

Syntax:

(make-honsed-sd-key [:pat <pat>] 
                    [:index <index>] 
                    [:orig <orig>])

This is identical to make-sd-key, except that we hons the structure we are creating.

Definition

This is an ordinary honsing make- macro introduced by defaggregate.

Macro: make-honsed-sd-key

(defmacro make-honsed-sd-key (&rest args)
  (std::make-aggregate 'sd-key
                       args '((:pat) (:index) (:orig))
                       'make-honsed-sd-key
                       t))