Word64.W64.to_nat: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/word64.bend as Word64
Lines 87-94 of bend-osdev-word64@0.1.1.0/word64.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&start_line=87&end_line=94

import Base

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.dbl