law out_pad

stelliferous@0.0.2.0 · proofs/u32_shift.bend:10

import Base

10law out_pad:
11  for +n: Nat
12  for +c: Bool
13  for +w: Word(n)
14  {Word.shl.out(1n+n,c,Word.shr.pad(n,w)) == (False{},Word.shl.put(1n+n,c,Word.shr.pad(n,w))) : Bool & Word(1n+n)}