		Search-engine friendly clone of the ACL2 documentation.

Vl-lintresult-p

Make-honsed-vl-lintresult

Constructor macro for honsed vl-lintresult-p structures.

Syntax:

(make-honsed-vl-lintresult [:design <design>] 
                           [:design0 <design0>] 
                           [:reportcard <reportcard>] 
                           [:sd-probs <sd-probs>])

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

Definition

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

Macro: make-honsed-vl-lintresult

(defmacro make-honsed-vl-lintresult (&rest args)
  (std::make-aggregate 'vl-lintresult
                       args
                       '((:design)
                         (:design0)
                         (:reportcard)
                         (:sd-probs))
                       'make-honsed-vl-lintresult
                       t))