law shl_out

lawful-words@0.1.0.0 · proof_u32.bend:617

import Base
import lawful-words@0.1.0.0/proof_word.bend as W

617law shl_out:
618  for +n: Nat
619  for +c: Bool
620  for +w: Word(n)
621  {Word.shl.out(n, c, w) == (W.stop(n, c, w), Word.shl.put(n, c, w)) : Bool & Word(n)}