Major Section: ACL2-BUILT-INS
(Expt r i) is the result of raising the number
r to the
The guard for
(expt r i) is that
r is a number and
is an integer, and furthermore, if
nonnegative. When the type requirements of the guard aren't
(expt r i) first coerces
r to a number and
i to an
Expt is a Common Lisp function. See any Common Lisp
documentation for more information. Note that
r can be a complex
number; this is consistent with Common lisp.
To see the ACL2 definition of this function, see pf.