def Digits.to_bytes

bend-trace-context@0.2.0.0 · src/digits.bend:84

import Base

84# The n bytes of 2n digits, most significant first: each byte takes the next
85# two digits, the first of them high.
86def Digits.to_bytes(n: Nat, digits: Digits(Nat.double(n))) -> List<&2, U32>:
87  match n:
88    case 0n:
89      Nil{}
90    case 1n+p:
91      match digits:
92        case DCon{high, DCon{low, rest}}:
93          Con{Digits.to_byte(DCon{high, DCon{low, DNil{}}}), Digits.to_bytes(p, rest)}