		Search-engine friendly clone of the ACL2 documentation.

Bip39

Bip39-entropy-size-p

Possible sizes of the entropy in bits.

These are the possible values of ENT in the table in [BIP39].

This is an ordinary std::defenum.

Function: bip39-entropy-size-p

(defun bip39-entropy-size-p (x)
  (declare (xargs :guard t))
  (or (eql x '128)
      (eql x '160)
      (eql x '192)
      (eql x '224)
      (eql x '256)))

Theorem: type-when-bip39-entropy-size-p

(defthm type-when-bip39-entropy-size-p
  (implies (bip39-entropy-size-p x)
           (if (integerp x) (< '1 x) 'nil))
  :rule-classes :compound-recognizer)