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).
