EXPT

exponential function
Major Section:  ACL2-BUILT-INS

(Expt r i) is the result of raising the number r to the integer power i.

The guard for (expt r i) is that r is a number and i is an integer, and furthermore, if r is 0 then i is nonnegative. When the type requirements of the guard aren't met, (expt r i) first coerces r to a number and i to an integer.

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.