		Search-engine friendly clone of the ACL2 documentation.

Flatnorm-res

Make-flatnorm-res

Basic constructor macro for flatnorm-res structures.

Syntax

(make-flatnorm-res [:assigns <assigns>] 
                   [:delays <delays>] 
                   [:constraints <constraints>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-flatnorm-res

(defmacro make-flatnorm-res (&rest args)
  (std::make-aggregate 'flatnorm-res
                       args
                       '((:assigns) (:delays) (:constraints))
                       'make-flatnorm-res
                       nil))

Function: flatnorm-res

(defun flatnorm-res (assigns delays constraints)
  (declare (xargs :guard (and (svex-alist-p assigns)
                              (svex-alist-p delays)
                              (constraintlist-p constraints))))
  (declare (xargs :guard t))
  (let ((__function__ 'flatnorm-res))
    (declare (ignorable __function__))
    (b* ((assigns (mbe :logic (svex-alist-fix assigns)
                       :exec assigns))
         (delays (mbe :logic (svex-alist-fix delays)
                      :exec delays))
         (constraints (mbe :logic (constraintlist-fix constraints)
                           :exec constraints)))
      (list (cons 'assigns assigns)
            (cons 'delays delays)
            (cons 'constraints constraints)))))