		Search-engine friendly clone of the ACL2 documentation.

Definterface-hash-infop

Make-honsed-definterface-hash-info

Constructor macro for honsed definterface-hash-infop structures.

Syntax:

(make-honsed-definterface-hash-info [:input-size-limit <input-size-limit>] 
                                    [:output-size <output-size>])

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

Definition

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

Macro: make-honsed-definterface-hash-info

(defmacro make-honsed-definterface-hash-info (&rest args)
  (std::make-aggregate 'definterface-hash-info
                       args
                       '((:input-size-limit) (:output-size))
                       'make-honsed-definterface-hash-info
                       t))