		Search-engine friendly clone of the ACL2 documentation.

Minor-frame

Make-minor-frame

Basic constructor macro for minor-frame structures.

Syntax

(make-minor-frame [:bindings <bindings>] 
                  [:scratch <scratch>] 
                  [:term <term>] 
                  [:term-index <term-index>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-minor-frame

(defmacro make-minor-frame (&rest args)
  (std::make-aggregate 'minor-frame
                       args
                       '((:bindings)
                         (:scratch)
                         (:term)
                         (:term-index))
                       'make-minor-frame
                       nil))

Function: minor-frame

(defun minor-frame (bindings scratch term term-index)
  (declare (xargs :guard (and (fgl-object-bindings-p bindings)
                              (scratchlist-p scratch)
                              (pseudo-termp term)
                              (acl2::maybe-natp term-index))))
  (declare (xargs :guard t))
  (let ((__function__ 'minor-frame))
    (declare (ignorable __function__))
    (b* ((bindings (mbe :logic (fgl-object-bindings-fix bindings)
                        :exec bindings))
         (scratch (mbe :logic (scratchlist-fix scratch)
                       :exec scratch))
         (term (mbe :logic (pseudo-term-fix term)
                    :exec term))
         (term-index (mbe :logic (acl2::maybe-natp-fix term-index)
                          :exec term-index)))
      (list (cons 'bindings bindings)
            (cons 'scratch scratch)
            (cons 'term term)
            (cons 'term-index term-index)))))