law put_into_zero

stelliferous@0.0.2.0 · proofs/word_power_of_two.bend:28

import Base

28law put_into_zero:
29  for +width: Nat
30  for +bit: Bool
31  {Word.shl.put(width,bit,Word.zero(width)) == Bool.pick(Word(width),bit,power(width,0n),Word.zero(width)) : Word(width)}