Word.hi_part: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as Word
Lines 254-262 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&start_line=254&end_line=262

import Base

# the bits of x above the low k
def hi_part(+n: Nat, +k: Nat, +x: Word(n)) -> Nat:
  match n k x:
    case 0n _ WNil{}:
      0n
    case 1n+p 0n WCon{b, t}:
      uw(1n+p, WCon{b, t})
    case 1n+p 1n+j WCon{b, t}:
      hi_part(p, j, t)

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=uw