all-vars-in-untranslated-term

(in-package "ACL2")

(define all-vars-in-untranslated-term
  (x (wrld plist-worldp))
  :returns (term "A @(tsee pseudo-termp).")
  :mode :program :parents (std/system/term-queries)
  :short "The variables free in the given untranslated term."
  :long (topstring (p "This function returns the variables of the given untranslated term.
     They are returned in reverse order of print occurrence,
     for consistency with the function, @(tsee all-vars).")
    (p "The input is translated for reasoning,
     so restrictions for executability are not enforced.
     There is also no restriction on the input being
     in @(':')@(tsee logic) mode."))
  (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))))))