		Search-engine friendly clone of the ACL2 documentation.

Backtrace-spec

Make-backtrace-spec

Basic constructor macro for backtrace-spec structures.

Syntax

(make-backtrace-spec [:rune <rune>] 
                     [:vars <vars>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-backtrace-spec

(defmacro make-backtrace-spec (&rest args)
  (std::make-aggregate 'backtrace-spec
                       args '((:rune) (:vars))
                       'make-backtrace-spec
                       nil))

Function: backtrace-spec

(defun backtrace-spec (rune vars)
  (declare (xargs :guard (and (maybe-fgl-generic-rune-p rune)
                              (pseudo-var-list-p vars))))
  (declare (xargs :guard t))
  (let ((__function__ 'backtrace-spec))
    (declare (ignorable __function__))
    (b* ((rune (mbe :logic (maybe-fgl-generic-rune-fix rune)
                    :exec rune))
         (vars (mbe :logic (pseudo-var-list-fix vars)
                    :exec vars)))
      (list rune vars))))