|
|
|---|
|
|
|
|---|
Define a function with a different low-level definition.
General Form: (defun-bridge name (formals) [:doc doc-string] [:loop-declare loop-decls] :loop loop-body [:raw-declare raw-decls] :raw raw-body)
This is much like executing
(defun name (formals) doc-string (declare (xargs :mode :program)) loop-decls loop-body)
in ACL2 and then
(defun name (formals) raw-decls raw-body)
in raw Lisp, except that extra checks and bookkeeping make it safer than that. An active ttag is required to use this form (See defttag), because it can easily corrupt ACL2 or render it unsound.