Trait BasePow2

pub trait BasePow2: Base {
    // Required methods
    spec fn bits() -> nat;
    proof fn bits_to_base();
}

Expand description

Represents a base which is a power of 2 specified by Self::bits().

Required Methods§

ensures

Self::bits() > 1,

Self::base() == pow2(Self::bits()),

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

{ 8 }

{ 64 }

{ usize::BITS as nat }