def negative_quotient

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

import Base

71def negative_quotient(n: Nat, word: Word(n), d: U32) -> Word(n):
72  match n:
73    case 0n: WNil{}
74    case 1n+ +p:
75      match word:
76        case WCon{bit, tail}:
77          from_nat(1n+p, Nat.sub(Nat.pow(2n, 1n+p), Nat.div(Nat.sub(Nat.pow(2n, 1n+p), unsigned(1n+p, WCon{bit, tail})), U32.to_nat(d))))