def from_nat

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

import Base

48# These mathematical definitions specify modulo arithmetic through Nat values,
49# independently of the implementation's ripple addition and binary long division.
50def from_nat(n: Nat, +value: Nat) -> Word(n):
51  match n:
52    case 0n:
53      WNil{}
54    case 1n+p:
55      WCon{Nat.is_eq(Nat.mod(value, 2n), 1n), from_nat(p, Nat.div(value, 2n))}