def shift_put

stelliferous@0.0.2.0 · proofs/word_arithmetic.bend:101

import Base

101def shift_put(+n: Nat,+w: Word(n)) -> {Word.shl(n,w) == Word.shl.put(n,False{},w) : Word(n)}:
102  match n:
103    case 0n:
104      {==}
105    case 1n+p:
106      WCon{b,t} = w
107      {==}