pub open spec fn pow2(e: nat) -> natExpand description
{ pow(2, e) as nat }This function computes 2 to the power of the given natural number e.
Note that the called function pow is opaque so the SMT solver doesn’t waste time
repeatedly recursively unfolding it.