PROOFText.wsh.pick: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
Lines 541-546 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=541&end_line=546

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

def wsh.pick(z: Bool, +a: W.W64, ez: {W.W64.is_zero(a) == z : Bool}) -> {Nat.read.go(W.W64.show.pick(z, a), 0n) == Some{W.W64.to_nat(a)} : Maybe<&2, Nat>}:
  match z:
    case True{}:
      Equal.cong(Nat, Maybe<&2, Nat>, zz => Some{zz}, 0n, W.W64.to_nat(a), Equal.sym(Nat, W.W64.to_nat(a), 0n, wsh.zv(a, ez)))
    case False{}:
      wsh.go(20n, a, "", wsh.f20(a))

Uses (13):
  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=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.f20
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.go
  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.is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.show.pick
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.to_nat