def w_shl

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32alg.bend:268

import Base

268def w_shl(+n: Nat, +w: Word(n)) -> {Word.shl(n, w) == Word.add(n, w, w) : Word(n)}:
269  match n:
270    case 0n:
271      match w:
272        case WNil{}:
273          {==}
274    case 1n+p:
275      match w:
276        case WCon{b, t}:
277          shl_adc(1n+p, WCon{b, t}, False{})