(vl-shell-entry events &key (state 'state)) → state
This command is defined in raw Lisp, see
Its argument is a list of ACL2 events to run before presenting the user with an interactive shell.
(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?") state)))