pub open spec fn pow2(e: nat) -> nat
{ 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.
e