		Search-engine friendly clone of the ACL2 documentation.

Outcomes

Outcome--make-myself

Signature
(outcome--make-myself obj) → retform
Arguments: obj — Guard (outcomep obj).
Returns: retform — Type (listp retform).

Definitions and Theorems

Function: outcome--make-myself

(defun outcome--make-myself (obj)
 (declare (xargs :guard (outcomep obj)))
 (let ((__function__ 'outcome--make-myself))
  (declare (ignorable __function__))
  (outcome-case
   obj
   :function-success
   (list 'make-outcome-function-success
         :message (outcome-function-success->message obj))
   :type-success (list 'make-outcome-type-success
                       :message (outcome-type-success->message obj))
   :specification-success
   (list 'make-outcome-specification-success
         :message (outcome-specification-success->message obj))
   :theorem-success
   (list 'make-outcome-theorem-success
         :message (outcome-theorem-success->message obj))
   :transformation-success
   (list 'make-outcome-transformation-success
         :message (outcome-transformation-success->message obj)
         :toplevels
         (toplevel-list--make-myself
              (outcome-transformation-success->toplevels obj)))
   :proof-obligation-failure
   (list
      'make-outcome-proof-obligation-failure
      :message (outcome-proof-obligation-failure->message obj)
      :obligation-expr
      (expression--make-myself
           (outcome-proof-obligation-failure->obligation-expr obj)))
   :theorem-failure
   (list 'make-outcome-theorem-failure
         :message (outcome-theorem-failure->message obj))
   :transformation-failure
   (list 'make-outcome-transformation-failure
         :message (outcome-transformation-failure->message obj))
   :unexpected-failure
   (list 'make-outcome-unexpected-failure
         :message (outcome-unexpected-failure->message obj)))))

Theorem: listp-of-outcome--make-myself

(defthm listp-of-outcome--make-myself
  (b* ((retform (outcome--make-myself obj)))
    (listp retform))
  :rule-classes :rewrite)