		Search-engine friendly clone of the ACL2 documentation.

Glcp-bit-ctrex-p

Make-honsed-glcp-bit-ctrex

Constructor macro for honsed glcp-bit-ctrex-p structures.

Syntax:

(make-honsed-glcp-bit-ctrex [:descrip <descrip>] 
                            [:env <env>] 
                            [:gvar-alist <gvar-alist>] 
                            [:dont-care-spec <dont-care-spec>])

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

Definition

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

Macro: make-honsed-glcp-bit-ctrex

(defmacro make-honsed-glcp-bit-ctrex (&rest args)
  (std::make-aggregate 'glcp-bit-ctrex
                       args
                       '((:descrip)
                         (:env)
                         (:gvar-alist)
                         (:dont-care-spec))
                       'make-honsed-glcp-bit-ctrex
                       t))