unquote-term

(in-package "ACL2")

(define unquote-term
  ((term (and (pseudo-termp term) (quotep term))))
  :returns value
  :parents (std/system)
  :short "Unquote a term that is a quoted constant."
  :long (topstring (p "The result is the quoted value, which may have any type.")
    (p "This has the same effect of @(tsee unquote) on terms,
     but it is a function instead of a macro and it has a guard."))
  (unquote term))

(define unquote-term-list
  ((terms (and (pseudo-term-listp terms) (quote-listp terms))))
  :returns (values true-listp)
  :parents (std/system unquote-term)
  :short "Lift @(tsee unquote-term) to lists."
  (cond ((endp terms) nil)
    (t (cons (unquote-term (car terms))
        (unquote-term-list (cdr terms))))))