		Search-engine friendly clone of the ACL2 documentation.

Hyp-tuple-p

Make-honsed-hyp-tuple

Constructor macro for honsed hyp-tuple-p structures.

Syntax:

(make-honsed-hyp-tuple [:name <name>] 
                       [:term <term>] 
                       [:alist <alist>])

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

Definition

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

Macro: make-honsed-hyp-tuple

(defmacro make-honsed-hyp-tuple (&rest args)
  (std::make-aggregate 'hyp-tuple
                       args '((:name) (:term) (:alist))
                       'make-honsed-hyp-tuple
                       t))