ACL2-PC::ACL2-WRAP

(macro) same as (lisp x)
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(acl2-wrap (pe :here))

General Form: (acl2-wrap form)

Same as (lisp form). This is provided for interface tools that want to be able to execute the same form in raw Lisp, in the proof-checker, or in the ACL2 top-level loop (lp).