|
|
|---|
|
|
|
|---|
Value:
" vl shell: Starts an interactive VL command loop (for experts). Usage: vl shell (there are no options) VL is built atop the ACL2 theorem prover. The VL shell gives you access to the ACL2 command loop, with all of the VL functions already built in. This is an advanced feature that is mainly intended for developers who are debugging and hacking on VL. "