def double_word

stelliferous@0.0.2.0 · proofs/word_arithmetic.bend:109

import Base

109def double_word(+n: Nat,+w: Word(n)) -> {Word.add(n,w,w) == Word.shl(n,w) : Word(n)}:
110  %Equal.sym(Word(n),Word.shl(n,w),Word.shl.put(n,False{},w),shift_put(n,w)) : {Word.add(n,w,w) == _ : Word(n)}
111  double_carry(n,w,False{})