Numeric.unsigned_quotient: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/lib/numeric.bend as Numeric
Lines 60-69 of bend-collections-laws-crypto@1.0.0.0/spec/lib/numeric.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/numeric.bend&start_line=60&end_line=69

import Base

# Observe the input constructor before evaluating mathematical division. This
# has the same from_nat(unsigned(input) / divisor) meaning; the structural guard
# keeps fixed large denominators from being expanded while input is unknown.
def unsigned_quotient(n: Nat, word: Word(n), d: U32) -> Word(n):
  match n:
    case 0n: WNil{}
    case 1n+ +p:
      match word:
        case WCon{bit, tail}:
          from_nat(1n+p, Nat.div(unsigned(1n+p, WCon{bit, tail}), U32.to_nat(d)))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_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/spec/lib/numeric.bend&name=from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/numeric.bend&name=unsigned