		Search-engine friendly clone of the ACL2 documentation.

Evmac-appcondp

Make-honsed-evmac-appcond

Constructor macro for honsed evmac-appcondp structures.

Syntax:

(make-honsed-evmac-appcond [:name <name>] 
                           [:formula <formula>])

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

Definition

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

Macro: make-honsed-evmac-appcond

(defmacro make-honsed-evmac-appcond (&rest args)
  (std::make-aggregate 'evmac-appcond
                       args '((:name) (:formula))
                       'make-honsed-evmac-appcond
                       t))