		Search-engine friendly clone of the ACL2 documentation.

Missing-parents

Interp-st-stack-full-backtrace

Produce a full backtrace for the FGL rewriter stack, containing all top-level bindings of all rules

Signature
(interp-st-stack-full-backtrace interp-st) → backtrace
Returns: backtrace — Type (backtrace-p backtrace).

Definitions and Theorems

Function: interp-st-stack-full-backtrace

(defun interp-st-stack-full-backtrace (interp-st)
  (declare (xargs :stobjs (interp-st)))
  (declare (xargs :guard t))
  (let ((__function__ 'interp-st-stack-full-backtrace))
    (declare (ignorable __function__))
    (stobj-let ((stack (interp-st->stack interp-st)))
               (bt)
               (stack-full-backtrace stack)
               bt)))

Theorem: backtrace-p-of-interp-st-stack-full-backtrace

(defthm backtrace-p-of-interp-st-stack-full-backtrace
  (b* ((backtrace (interp-st-stack-full-backtrace interp-st)))
    (backtrace-p backtrace))
  :rule-classes :rewrite)