def W64.to_nat

bend-osdev-word64@0.1.1.0 · word64.bend:87

import Base

87# lo + hi * 2^32. The high half's weight is 32 doublings of its value, not a
88# product with the closed number 2^32: the checkers count a Nat in unary, so
89# a proof that unfolds to_nat on unknown halves stays symbolic this way
90# (see README.md, Laws).
91def W64.to_nat(a: W64) -> Nat:
92  match a:
93    case W64{h, l}:
94      Nat.add(U32.to_nat(l), W64.dbl(32n, U32.to_nat(h)))