def Ops.pow2

bend-collections-laws-crypto@1.0.0.0 · spec/math/instances.bend:72

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/math/num.bend as N

72def Ops.pow2(~T: Data, ~op: N.Op<T> -> T, ~val: T -> Nat, +w: Nat, +k: Nat, +hk: {Nat.is_lt(k, w) == True{} : Bool}) -> Type:
73  {val(op(N.Pow2{k})) == C.pow2(k) : Nat}