		Search-engine friendly clone of the ACL2 documentation.

Std/system

Unquote-term

Unquote a term that is a quoted constant.

Signature
(unquote-term term) → value
Arguments: term — Guard (and (pseudo-termp term) (quotep term)).

The result is the quoted value, which may have any type.

This has the same effect of unquote on terms, but it is a function instead of a macro and it has a guard.

Definitions and Theorems

Function: unquote-term

(defun unquote-term (term)
  (declare (xargs :guard (and (pseudo-termp term)
                              (quotep term))))
  (let ((__function__ 'unquote-term))
    (declare (ignorable __function__))
    (unquote term)))

Subtopics

Unquote-term-list: Lift unquote-term to lists.