pseudo-command-formp

(in-package "ACL2")

(defsection pseudo-command-formp
  :parents (system-utilities-non-built-in)
  :short "Recognize well-formed command forms."
  :long "<p>We see no reasonable way to restrict the form of a command,
      other than to insist that it is a true list.</p>"
  (defun pseudo-command-formp
    (x)
    (declare (xargs :guard t))
    (true-listp x)))