		Search-engine friendly clone of the ACL2 documentation.

Parametrize-config

Make-parametrize-config

Basic constructor macro for parametrize-config structures.

Syntax

(make-parametrize-config [:build-limit <build-limit>] 
                         [:conjoin-limit <conjoin-limit>] 
                         [:output-types <output-types>])

This is the usual way to construct parametrize-config structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-parametrize-config

(defmacro make-parametrize-config (&rest args)
  (std::make-aggregate 'parametrize-config
                       args
                       '((:build-limit)
                         (:conjoin-limit)
                         (:output-types))
                       'make-parametrize-config
                       nil))

Function: parametrize-config

(defun parametrize-config (build-limit conjoin-limit output-types)
 (declare
  (xargs :guard (and (natp build-limit)
                     (natp conjoin-limit)
                     (parametrize-output-type-map-p output-types))))
 (declare (xargs :guard t))
 (let ((__function__ 'parametrize-config))
  (declare (ignorable __function__))
  (b*
   ((build-limit (mbe :logic (nfix build-limit)
                      :exec build-limit))
    (conjoin-limit (mbe :logic (nfix conjoin-limit)
                        :exec conjoin-limit))
    (output-types
         (mbe :logic (parametrize-output-type-map-fix output-types)
              :exec output-types)))
   (cons
    :parametrize-config (list (cons 'build-limit build-limit)
                              (cons 'conjoin-limit conjoin-limit)
                              (cons 'output-types output-types))))))