ACL2-PC_colon__colon_ACL2-WRAP.html -- ACL2 Version 3.1

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