Set-measure-function
Set the default measure function symbol
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 name is 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 and encapsulate events in which it occurs; see ACL2-defaults-table. Although this is
thus an event (see table), nevertheless no output results from a
set-measure-function event.
This event sets the default measure function to name. Subsequently,
if a recursively defined function is submitted to defun with no
explicitly given :measure argument, defun ``guesses'' the measure
(name var), where name is the then current default measure function
and var is the first formal found to be tested along every branch and
changed in every recursive call.
Note that if (table acl2-defaults-table :measure-function 'name) has
its default value of nil, then the default measure function is ACL2-count.
