		Search-engine friendly clone of the ACL2 documentation.

Fact-infop

Make-honsed-fact-info

Constructor macro for honsed fact-infop structures.

Syntax:

(make-honsed-fact-info [:thm-name <thm-name>] 
                       [:formula <formula>])

This is identical to make-fact-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-fact-info

(defmacro make-honsed-fact-info (&rest args)
  (std::make-aggregate 'fact-info
                       args '((:thm-name) (:formula))
                       'make-honsed-fact-info
                       t))