def unsigned_quotient

bend-collections-laws-crypto@1.0.0.0 · spec/lib/numeric.bend:60

import Base

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