|
|
|---|
|
|
|
|---|
Execute some events with only the specified fns and/or vars temporarily touchable.
Examples: (progn=touchable :all ; same as :fns :all :vars :all (defun foo ...) (defun bar ...)) (progn=touchable :vars (current-package ld-skip-proofsp) ; :fns () implied ...) (progn=touchable :fns :all ; :vars () implied ...) (progn=touchable :fns set-w :vars :all ...)
This is like progn except that it surrounds the events with code to set only certain fns and/or vars as 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.