		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Expt2

(expt2 n) is the same as (expt 2 n), except that it coerces its argument to a natural.

Signature
(expt2 n) → nat
Arguments: n — Guard (natp n).
Returns: nat — Type (natp nat).

Definitions and Theorems

Function: expt2$inline

(defun expt2$inline (n)
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'expt2))
    (declare (ignorable __function__))
    (mbe :logic (expt 2 (nfix n))
         :exec (the unsigned-byte
                    (ash 1 (the unsigned-byte n))))))

Theorem: expt2-type

(defthm expt2-type
  (b* ((nat (expt2$inline n))) (natp nat))
  :rule-classes :type-prescription)