## SET-MEASURE-FUNCTION

set the default measure function symbol
Major Section: SWITCHES-PARAMETERS-AND-MODES

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`

.