		Search-engine friendly clone of the ACL2 documentation.

Backtrace

Backtrace-to-obj

Turn a FGL backtrace into a proper symbolic object

Signature
(backtrace-to-obj x) → obj
Arguments: x — Guard (backtrace-p x).
Returns: obj — Type (fgl-object-p obj).

Definitions and Theorems

Function: backtrace-to-obj

(defun backtrace-to-obj (x)
  (declare (xargs :guard (backtrace-p x)))
  (let ((__function__ 'backtrace-to-obj))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (g-cons (backtrace-frame-to-obj (car x))
              (backtrace-to-obj (cdr x))))))

Theorem: fgl-object-p-of-backtrace-to-obj

(defthm fgl-object-p-of-backtrace-to-obj
  (b* ((obj (backtrace-to-obj x)))
    (fgl-object-p obj))
  :rule-classes :rewrite)