		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

All-vars-in-untranslated-term

The variables free in the given untranslated term.

Signature
(all-vars-in-untranslated-term x wrld) → term
Arguments: wrld — Guard (plist-worldp wrld).
Returns: term — A pseudo-termp.

This function returns the variables of the given untranslated term. They are returned in reverse order of print occurrence, for consistency with the function, all-vars.

The input is translated for reasoning, so restrictions for executability are not enforced. There is also no restriction on the input being in :logic mode.

Definitions and Theorems

Function: all-vars-in-untranslated-term

(defun all-vars-in-untranslated-term (x wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (let ((__function__ 'all-vars-in-untranslated-term))
    (declare (ignorable __function__))
    (let ((ctx 'all-vars-in-untranslated-term))
      (mv-let (erp term)
              (translate-cmp x t nil
                             nil ctx wrld (default-state-vars nil))
        (cond (erp (er hard erp "~@0" term))
              (t (all-vars term)))))))