def put

stelliferous@0.0.2.0 · proofs/word_multiplication.bend:44

import Base

44def put(+n: Nat,+b: Bool,+w: Word(n)) -> {Word.shl.put(n,b,w) == truncate(n,WCon{b,w}) : Word(n)}:
45  match n:
46    case 0n:
47      {==}
48    case 1n+ +p:
49      WCon{+c,+t} = w
50      %put(p,c,t) : {WCon{b,Word.shl.put(p,c,t)} == WCon{b,_} : Word(1n+p)}
51      {==}