def hi_part

bend-collections-laws-math@1.0.0.0 · proofs/lib/word.bend:254

import Base

254# the bits of x above the low k
255def hi_part(+n: Nat, +k: Nat, +x: Word(n)) -> Nat:
256  match n k x:
257    case 0n _ WNil{}:
258      0n
259    case 1n+p 0n WCon{b, t}:
260      uw(1n+p, WCon{b, t})
261    case 1n+p 1n+j WCon{b, t}:
262      hi_part(p, j, t)