def put_inc

stelliferous@0.0.2.0 · proofs/u32_shift.bend:41

import Base

41def put_inc(+n: Nat,+w: Word(n)) -> {Word.shl.put(n,True{},w) == Word.inc(n,Word.shl(n,w)) : Word(n)}:
42  match n:
43    case 0n:
44      {==}
45    case 1n+p:
46      WCon{bit,tail} = w
47      {==}