def wsh.pick

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:541

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

541def 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>}:
542  match z:
543    case True{}:
544      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)))
545    case False{}:
546      wsh.go(20n, a, "", wsh.f20(a))