Function vstd::arithmetic::power2::pow2

source · 
pub open spec fn pow2(e: nat) -> nat
Expand description
{ pow(2, e) as nat }

This function computes 2 to the power of the given natural number e. It’s opaque so that the SMT solver doesn’t waste time repeatedly recursively unfolding it.