		Search-engine friendly clone of the ACL2 documentation.

Vl-shell

Vl-shell-top

Top-level vl shell command.

Signature
(vl-shell-top argv &key (state 'state)) → state
Arguments: argv — Guard (string-listp argv).

This command just calls vl-shell-entry. It provides a single event that saves the user arguments as an ACL2 constant named vl::*vl-shell-argv*.

Definitions and Theorems

Function: vl-shell-top-fn

(defun vl-shell-top-fn (argv state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (string-listp argv)))
  (let ((__function__ 'vl-shell-top))
    (declare (ignorable __function__))
    (vl-shell-entry
         (cons (cons 'defconst
                     (cons '*vl-shell-argv*
                           (cons (cons 'quote (cons argv 'nil))
                                 'nil)))
               'nil))))