def shl_out

bend-collections-laws-math@1.0.0.0 · proofs/lib/word.bend:118

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

118# the out-shifted bit and word together hold c + 2w
119def shl_out(+n: Nat, +c: Bool, +w: Word(n)) -> {Nat.add(S.unsigned(n, ow(n, Word.shl.out(n, c, w))), S.scale_binary(n, S.bit_value(ob(n, Word.shl.out(n, c, w))))) == Nat.add(S.bit_value(c), Nat.double(S.unsigned(n, w))) : Nat}:
120  match n w:
121    case 0n WNil{}:
122      shl_nil(c)
123    case 1n+p WCon{b, tl}:
124      shl_con(p, c, b, tl, Word.shl.out(p, b, tl), shl_out(p, b, tl))