def shl_nil

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

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

111def shl_nil(+c: Bool) -> {Nat.add(S.unsigned(0n, ow(0n, Word.shl.out(0n, c, WNil{}))), S.scale_binary(0n, S.bit_value(ob(0n, Word.shl.out(0n, c, WNil{}))))) == Nat.add(S.bit_value(c), Nat.double(S.unsigned(0n, WNil{}))) : Nat}:
112  match c:
113    case True{}:
114      {==}
115    case False{}:
116      {==}