Expt
Exponential function
(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.
Function: expt
(defun expt (r i)
(declare (xargs :guard (and (acl2-numberp r)
(integerp i)
(not (and (eql r 0) (< i 0))))))
(cond ((zip i) 1)
((= (fix r) 0) 0)
((> i 0) (* r (expt r (+ i -1))))
(t (* (/ r) (expt r (+ i 1))))))Subtopics
- Basic-expt-normalization
- Basic rules for normalizing and simplifying exponents.
- Basic-expt-type-rules
- Rules about when expt produces integers, positive numbers, etc.
