		Search-engine friendly clone of the ACL2 documentation.

Eoutcome

Make-eoutcome

Basic constructor macro for eoutcome structures.

Syntax

(make-eoutcome [:cstate <cstate>] 
               [:values <values>])

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

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

Definition

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

Macro: make-eoutcome

(defmacro make-eoutcome (&rest args)
  (std::make-aggregate 'eoutcome
                       args '((:cstate) (:values))
                       'make-eoutcome
                       nil))

Function: eoutcome

(defun eoutcome (cstate values)
  (declare (xargs :guard (and (cstatep cstate)
                              (value-listp values))))
  (declare (xargs :guard t))
  (let ((__function__ 'eoutcome))
    (declare (ignorable __function__))
    (b* ((cstate (mbe :logic (cstate-fix cstate)
                      :exec cstate))
         (values (mbe :logic (value-list-fix values)
                      :exec values)))
      (cons :eoutcome (list (cons 'cstate cstate)
                            (cons 'values values))))))