|
|
|---|
|
|
|
|---|
Execute some events with some additional fns and/or vars made temporarily touchable.
Examples: (progn+touchable :all ; same as :fns :all :vars :all (defun foo ...) (defun bar ...)) (progn+touchable :vars (current-package ld-skip-proofsp) ...) (progn+touchable :fns :all ...) (progn+touchable :fns set-w :vars :all ...)
This is like progn except that it surrounds the events with code to add certain fns and/or vars to those that are temporarily touchable. Related to progn=touchable. An active ttag is required to use this form (See defttag) because it can render ACL2 unsound (See remove-untouchable). Note that the syntax for this macro is not quite like traditional keyword arguments, which would come at the end of the argument list.