		Search-engine friendly clone of the ACL2 documentation.

Termp

recognizer for the quotation of a term

Example:
(termp '(CAR (CONS X Y)) (w state))

General Form:
(termp x w)

where x is any ACL2 object and w is an ACL2 logical world. The result is t or nil according to whether x is the quotation of a translated (well-formed) term in the world, w. See term for a discussion of translated terms.

Each metafunction (see meta) is supposed to take (the quotation of) a translated term as input and yield (the quotation of) a translated term as output. When a metafunction is run by the simplifier its input is guaranteed to be well-formed by invariants maintained by ACL2. But its output is checked by an explicit call of termp unless the user has proved that the metafunction always returns a term (see well-formedness-guarantee) or has taken the risk of disabling the runtime test with set-skip-meta-termp-checks.

Termp is mutually recursive with term-listp.

Function: termp

(defun termp (x w)
  (declare (xargs :guard (plist-worldp-with-formals w)))
  (cond ((atom x) (legal-variablep x))
        ((eq (car x) 'quote)
         (and (consp (cdr x)) (null (cddr x))))
        ((symbolp (car x))
         (let ((arity (arity (car x) w)))
           (and arity (term-listp (cdr x) w)
                (eql (length (cdr x)) arity))))
        ((and (consp (car x))
              (true-listp (car x))
              (eq (car (car x)) 'lambda)
              (eql 3 (length (car x)))
              (arglistp (cadr (car x)))
              (termp (caddr (car x)) w)
              (null (set-difference-eq (all-vars (caddr (car x)))
                                       (cadr (car x))))
              (term-listp (cdr x) w)
              (eql (length (cadr (car x)))
                   (length (cdr x))))
         t)
        (t nil)))

Function: term-listp

(defun term-listp (x w)
  (declare (xargs :guard (plist-worldp-with-formals w)))
  (cond ((atom x) (equal x nil))
        ((termp (car x) w)
         (term-listp (cdr x) w))
        (t nil)))

Subtopics

Logic-fns-list-listp: Recognizer for when a given list of lists of terms calls only :logic-mode function symbols
Logic-fnsp: Recognizer for when a given term calls only :logic-mode function symbols
Logic-fns-listp: Recognizer for when a given list of terms calls only :logic-mode function symbols
Logic-termp: Recognizer for terms that call only :logic-mode function symbols
Logic-term-list-listp: Recognizer for lists of lists of terms that call only :logic-mode function symbols
Logic-term-listp: Recognizer for lists of terms that call only :logic-mode function symbols