		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)))))