Bin.shr: def of bend-lawful-stdlib@0.1.0.0
Import: import bend-lawful-stdlib@0.1.0.0/src/float/bin.bend as Bin
Lines 199-212 of bend-lawful-stdlib@0.1.0.0/src/float/bin.bend: https://jend.leeeet.dev/read.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&start_line=199&end_line=212

import Base

# a / 2^k, with the last bit shifted out (round) and whether any bit
# below it was set (sticky); r and s are the bits already shifted out
def shr(k: Nat, a: Bin, r: Bool, s: Bool) -> Bin & Bool & Bool:
  match k:
    case 0n:
      (a, r, s)
    case 1n+j:
      match a:
        case BZ{}:
          shr(j, BZ{}, False{}, Bool.or(r, s))
        case B0{x}:
          shr(j, x, False{}, Bool.or(r, s))
        case B1{x}:
          shr(j, x, True{}, Bool.or(r, s))

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=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=Bin