		Search-engine friendly clone of the ACL2 documentation.

Config-p

Make-config

Constructor macro for config-p structures.

Syntax:

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

This is our preferred way to construct config-p structures. It simply conses together a structure with the specified fields.

This macro generates a new config-p structure from scratch. See also change-config, which can "change" an existing structure, instead.

The config-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-config instead.

Definition

This is an ordinary make- macro introduced by defaggregate.

Macro: make-config

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