		Search-engine friendly clone of the ACL2 documentation.

Boundrw-subst-p

Make-honsed-boundrw-subst

Constructor macro for honsed boundrw-subst-p structures.

Syntax:

(make-honsed-boundrw-subst [:lhs <lhs>] 
                           [:rhs <rhs>] 
                           [:alist <alist>])

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

Definition

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

Macro: make-honsed-boundrw-subst

(defmacro make-honsed-boundrw-subst (&rest args)
  (std::make-aggregate 'boundrw-subst
                       args '((:lhs) (:rhs) (:alist))
                       'make-honsed-boundrw-subst
                       t))