The variables free in the given untranslated term.
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
(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)))))))