		Search-engine friendly clone of the ACL2 documentation.

System-utilities-non-built-in

Pseudo-command-landmarkp

Recognize command landmarks in the ACL2 world.

Warning: Keep this in sync with (defrec command-tuple ...) in the ACL2 sources.

Definitions and Theorems

Function: pseudo-command-landmarkp

(defun pseudo-command-landmarkp (val)
  (declare (xargs :guard t))
  (and (consp val)
       (or (eql (car val) -1) (natp (car val)))
       (consp (cdr val))
       (consp (cadr val))
       (if (keywordp (car (cadr val)))
           (and (eq (car (cadr val)) :logic)
                (pseudo-command-formp (cdr (cadr val))))
         (pseudo-command-formp (cadr val)))
       (consp (cddr val))
       (or (null (caddr val))
           (stringp (caddr val)))
       (or (null (cdddr val))
           (pseudo-command-formp (cdddr val)))))