def put_pad

stelliferous@0.0.2.0 · proofs/u32_shift.bend:72

import Base

72def put_pad(+n: Nat,+c: Bool,+w: Word(n)) -> {Word.shl.put(1n+n,c,Word.shr.pad(n,w)) == WCon{c,w} : Word(1n+n)}:
73  match n:
74    case 0n:
75      WNil{} = w
76      {==}
77    case 1n+ +p:
78      WCon{+b,+tail} = w
79      %put_pad(p,b,tail) : {WCon{c,Word.shl.put(1n+p,b,Word.shr.pad(p,tail))} == WCon{c,_} : Word(2n+p)}
80      {==}