		Search-engine friendly clone of the ACL2 documentation.

Hyppair-p

Make-honsed-hyppair

Constructor macro for honsed hyppair-p structures.

Syntax:

(make-honsed-hyppair [:bfr-mode <bfr-mode>] 
                     [:hyp <hyp>])

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

Definition

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

Macro: make-honsed-hyppair

(defmacro make-honsed-hyppair (&rest args)
  (std::make-aggregate 'hyppair
                       args '((:bfr-mode) (:hyp))
                       'make-honsed-hyppair
                       t))