U32.U32Word.mask: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/u32.bend as U32
Lines 72-83 of bend-osdev-u32@0.1.0.0/u32.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&start_line=72&end_line=83

import Base

# the word of width n whose low k bits are set (2^k - 1, for k <= n): the
# mask that U32.and(x, m) takes x's low k bits with
def U32Word.mask(n: Nat, k: Nat) -> Word(n):
  match n:
    case 0n:
      WNil{}
    case 1n+p:
      match k:
        case 0n:
          Word.zero(1n+p)
        case 1n+j:
          WCon{True{}, U32Word.mask(p, j)}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Base/base.bend&name=Word.zero