		Search-engine friendly clone of the ACL2 documentation.

Api+senv

Make-api+senv

Basic constructor macro for api+senv structures.

Syntax

(make-api+senv [:api <api>] 
               [:senv <senv>])

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

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

Definition

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

Macro: make-api+senv

(defmacro make-api+senv (&rest args)
  (std::make-aggregate 'api+senv
                       args '((:api) (:senv))
                       'make-api+senv
                       nil))

Function: api+senv

(defun api+senv (api senv)
  (declare (xargs :guard (and (apip api) (senvp senv))))
  (declare (xargs :guard t))
  (let ((__function__ 'api+senv))
    (declare (ignorable __function__))
    (b* ((api (mbe :logic (api-fix api) :exec api))
         (senv (mbe :logic (senv-fix senv)
                    :exec senv)))
      (cons :api+senv (list (cons 'api api)
                            (cons 'senv senv))))))