Major Section: EVENTS
Examples: (set-measure-function nqthm::count)Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
General Form: (set-measure-function name)where
nameis a function symbol of one argument. This macro is equivalent to
(table acl2-defaults-table :measure-function 'name), and hence is local to any books in which is occurs; see acl2-defaults-table. Although this is thus an event (see table), nevertheless no output results from a
This event sets the default measure function to
if a recursively defined function is submitted to
defun with no
defun ``guesses'' the measure
(name var), where
name is the then current default measure function
var is the first formal found to be tested along every branch
and changed in every recursive call.