Implementation-level vl shell command.
(vl-shell-entry events &key (state 'state)) → state
- events — Guard (true-listp events).
This command is defined in raw Lisp, see shell-raw.lsp for
Its argument is a list of ACL2 events to run before presenting the user with
an interactive shell.
Definitions and Theorems
(defun vl-shell-entry-fn (events state)
(declare (xargs :stobjs (state)))
(declare (xargs :guard (true-listp events)))
(let ((__function__ 'vl-shell-entry))
(declare (ignorable __function__))
(progn$ (die "Raw lisp definition not installed?")