WordArithmetic.encode: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
Lines 53-58 of stelliferous@0.0.2.0/proofs/word_arithmetic.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_arithmetic.bend&start_line=53&end_line=58

import Base

def encode(a: Nat,+width: Nat) -> Word(width):
  match a:
    case 0n:
      Word.zero(width)
    case 1n+p:
      Word.inc(width,encode(p,width))

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.inc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero