		Search-engine friendly clone of the ACL2 documentation.

Vls-commands

Vls-command-arg-to-eformal

Signature
(vls-command-arg-to-eformal arg) → *
Arguments: arg — Guard (symbolp arg).

Definitions and Theorems

Function: vls-command-arg-to-eformal

(defun vls-command-arg-to-eformal (arg)
  (declare (xargs :guard (symbolp arg)))
  (let ((__function__ 'vls-command-arg-to-eformal))
    (declare (ignorable __function__))
    (list arg
          (if (equal arg 'data)
              'vls-data-p
            'stringp))))