		Search-engine friendly clone of the ACL2 documentation.

Printconfig

Make-printconfig

Basic constructor macro for printconfig structures.

Syntax

(make-printconfig [:flat-right-margin <flat-right-margin>] 
                  [:hard-right-margin <hard-right-margin>] 
                  [:print-base <print-base>] 
                  [:print-radix <print-radix>] 
                  [:home-package <home-package>] 
                  [:print-lowercase <print-lowercase>])

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

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

Definition

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

Macro: make-printconfig

(defmacro make-printconfig (&rest args)
  (std::make-aggregate 'printconfig
                       args
                       '((:flat-right-margin . 40)
                         (:hard-right-margin . 77)
                         (:print-base . 10)
                         (:print-radix)
                         (:home-package pkg-witness "ACL2")
                         (:print-lowercase))
                       'make-printconfig
                       nil))

Function: printconfig

(defun printconfig
       (flat-right-margin hard-right-margin print-base print-radix
                          home-package print-lowercase)
 (declare (xargs :guard (and (posp flat-right-margin)
                             (posp hard-right-margin)
                             (print-base-p print-base)
                             (booleanp print-radix)
                             (symbolp home-package)
                             (booleanp print-lowercase))))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'printconfig))
  (declare (ignorable acl2::__function__))
  (b*
   ((flat-right-margin (mbe :logic (acl2::pos-fix flat-right-margin)
                            :exec flat-right-margin))
    (hard-right-margin (mbe :logic (acl2::pos-fix hard-right-margin)
                            :exec hard-right-margin))
    (print-base (mbe :logic (print-base-fix print-base)
                     :exec print-base))
    (print-radix (mbe :logic (acl2::bool-fix print-radix)
                      :exec print-radix))
    (home-package (mbe :logic (acl2::symbol-fix home-package)
                       :exec home-package))
    (print-lowercase (mbe :logic (acl2::bool-fix print-lowercase)
                          :exec print-lowercase)))
   (cons
    :printconfig
    (std::prod-cons
      (std::prod-cons flat-right-margin
                      (std::prod-cons hard-right-margin print-base))
      (std::prod-cons
           print-radix
           (std::prod-cons home-package print-lowercase)))))))