PROOFText.wsh.go: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
Lines 410-415 of bend-osdev-word64@0.1.1.0/PROOF_text.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&start_line=410&end_line=415

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W

def wsh.go(n: Nat, +a: W.W64, +acc: String, +hf: {W.W64.is_zero(wsh.it(n, a)) == True{} : Bool}) -> {Nat.read.go(W.W64.show.go(n, a, acc), 0n) == Nat.read.go(acc, W.W64.to_nat(a)) : Maybe<&2, Nat>}:
  match n:
    case 0n:
      Equal.cong(Nat, Maybe<&2, Nat>, zz => Nat.read.go(acc, zz), 0n, W.W64.to_nat(a), Equal.sym(Nat, W.W64.to_nat(a), 0n, wsh.zv(a, hf)))
    case 1n+ +p:
      wsh.step(p, a, acc, W.W64.is_zero(a), {==}, wsh.go(p, wsh.q(a), acc, hf), wsh.go(p, wsh.q(a), SCon{W.W64.digit(wsh.r(a)), acc}, hf))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.read.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.it
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.q
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.step
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.zv
  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.digit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.show.go
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.to_nat