def w64.lo_cat

bend-osdev-algo@0.1.0.0 · PROOF.bend:537

import Base
import bend-osdev-word64@0.1.0.0/word64.bend as W

537def w64.lo_cat(m: Nat, +n: Nat, l: Word(m), +h: Word(n)) -> {W.W64.bits.lo(m, n, W.W64.bits.cat(m, n, l, h)) == l : Word(m)}:
538  match m:
539    case 0n:
540      match l:
541        case WNil{}:
542          {==}
543    case 1n+ +p:
544      match l:
545        case WCon{+b, +t}:
546          %w64.lo_cat(p, n, t, h) : {WCon{b, W.W64.bits.lo(p, n, W.W64.bits.cat(p, n, t, h))} == WCon{b, _} : Word(1n+p)}
547          {==}