def ops_pow2

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32laws.bend:353

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/instances.bend as SI
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X

353def ops_pow2(+k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> SI.Ops.pow2(~U32, ~I.u32_op, ~SG.u32_val, 32n, k, hk):
354  %Equal.sym(U32, X.pow2(k), U32{WD.pw(32n, k)}, pw_table(k, hk)) : {v(_) == C.pow2(k) : Nat}
355  %Equal.sym(Nat, C.pow2(k), WD.sc(k, 1n), U.pow2_scale(k)) : {v(U32{WD.pw(32n, k)}) == _ : Nat}
356  PD.pow32(k, hk, 1n, {==}, U32{WD.pw(32n, k)}, {==})