		Search-engine friendly clone of the ACL2 documentation.

Quote-term

Build a quoted constant term with the given value.

Function: quote-term

(defun quote-term (x)
  (declare (xargs :guard t))
  (let ((__function__ 'quote-term))
    (declare (ignorable __function__))
    (list 'quote x)))

Theorem: pseudo-termp-of-quote-term

(defthm pseudo-termp-of-quote-term
  (b* ((term (quote-term x)))
    (pseudo-termp term))
  :rule-classes :rewrite)

Theorem: quotep-of-quote-term

(defthm quotep-of-quote-term
  (b* nil (quotep (quote-term x))))