		Search-engine friendly clone of the ACL2 documentation.

Flatnorm-setup

Make-flatnorm-setup

Basic constructor macro for flatnorm-setup structures.

Syntax

(make-flatnorm-setup [:monotonify <monotonify>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-flatnorm-setup

(defmacro make-flatnorm-setup (&rest args)
  (std::make-aggregate 'flatnorm-setup
                       args '((:monotonify))
                       'make-flatnorm-setup
                       nil))

Function: flatnorm-setup

(defun flatnorm-setup (monotonify)
  (declare (xargs :guard (booleanp monotonify)))
  (declare (xargs :guard t))
  (let ((__function__ 'flatnorm-setup))
    (declare (ignorable __function__))
    (b* ((monotonify (mbe :logic (bool-fix monotonify)
                          :exec monotonify)))
      (list (cons 'monotonify monotonify)))))