def AP.shl_put

bend-osdev-array@0.1.0.1 · PROOF.bend:375

import Base

375def AP.shl_put(n: Nat, w: Word(n)) -> {Word.shl(n, w) == Word.shl.put(n, False{}, w) : Word(n)}:
376  match n:
377    case 0n:
378      {==}
379    case 1n+q:
380      match w:
381        case WCon{b, t}:
382          {==}