		Search-engine friendly clone of the ACL2 documentation.

Backtrace

Backtrace-frame-to-obj

Turn a FGL backtrace frame into a proper symbolic object

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

Definitions and Theorems

Function: backtrace-frame-to-obj

(defun backtrace-frame-to-obj (x)
  (declare (xargs :guard (backtrace-frame-p x)))
  (let ((__function__ 'backtrace-frame-to-obj))
    (declare (ignorable __function__))
    (b* (((backtrace-frame x)))
      (g-cons (g-concrete x.index)
              (g-cons (g-concrete x.rune)
                      (g-cons (g-map '(:g-map) x.objs)
                              nil))))))

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

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