law shr_big

bend-osdev-word64@0.1.1.0 · LAWS.bend:184

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W

184law shr_big:
185  for +a: W.W64
186  for +k: Nat
187  for +h: {Nat.is_le(64n, k) == True{} : Bool}
188  {W.W64.shr(a, k) == W.W64.zero() : W.W64}