~/jendhub

def mod_sh

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:555

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as F64round
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/proofs/math/typed/width.bend as WW

555def mod_sh(+k: Nat, +x: Nat) -> {Nat.mod(C.shift(1n+k, x), 2n) == 0n : Nat}:
556  WW.odd_limb(k, 0n, x)

Uses (4)

Used by (1)