		Search-engine friendly clone of the ACL2 documentation.

Bip39-entropyp

Recognizer for bip39-entropy.

Function: bip39-entropyp

(defun bip39-entropyp (x)
  (declare (xargs :guard t))
  (and (bit-listp x)
       (bip39-entropy-size-p (len x))
       t))

Theorem: booleanp-of-bip39-entropyp

(defthm booleanp-of-bip39-entropyp
  (b* ((yes/no (bip39-entropyp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)