Untranslated-expr-calls-some-fn
- Signature
(untranslated-expr-calls-some-fn fns term wrld) → *
- Arguments
- fns — Guard (symbol-listp fns).
- wrld — Guard (plist-worldp wrld).
Definitions and Theorems
Function: untranslated-expr-calls-some-fn
(defun untranslated-expr-calls-some-fn (fns term wrld)
(declare (xargs :guard (and (symbol-listp fns)
(plist-worldp wrld))))
(let ((__function__ 'untranslated-expr-calls-some-fn))
(declare (ignorable __function__))
(acl2::expr-calls-some-fn fns
(acl2::translate-term term 'top wrld))))
