~/jendhub

def w64.hi_cat

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

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

549def w64.hi_cat(m: Nat, +n: Nat, l: Word(m), +h: Word(n)) -> {W.W64.bits.hi(m, n, W.W64.bits.cat(m, n, l, h)) == h : Word(n)}:
550  match m:
551    case 0n:
552      match l:
553        case WNil{}:
554          {==}
555    case 1n+ +p:
556      match l:
557        case WCon{b, +t}:
558          w64.hi_cat(p, n, t, h)

Uses (6)

Used by (1)