		Search-engine friendly clone of the ACL2 documentation.

Config-p

Make-honsed-config

Constructor macro for honsed config-p structures.

Syntax:

(make-honsed-config [:cmdline <cmdline>] 
                    [:verbose <verbose>] 
                    [:timing <timing>] 
                    [:mintime <mintime>] 
                    [:remove-temps <remove-temps>] 
                    [:lrat-check <lrat-check>])

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

Definition

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

Macro: make-honsed-config

(defmacro make-honsed-config (&rest args)
  (std::make-aggregate 'config
                       args
                       '((:cmdline)
                         (:verbose)
                         (:timing . t)
                         (:mintime)
                         (:remove-temps)
                         (:lrat-check))
                       'make-honsed-config
                       t))