Fmt.Short.finite.go: def of bend-kit-fmt@0.1.0.0
Import: import bend-kit-fmt@0.1.0.0/fmt.bend as Fmt
Lines 403-414 of bend-kit-fmt@0.1.0.0/fmt.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&start_line=403&end_line=414

import Base

# v = f * 2^(be - 150); a power-of-two f above the least exponent has a
# nearer lower neighbour, so t = 1 there. A and B are the positive and
# negative parts of the binary exponent.
def Short.finite.go(+f: U32, +be: U32, t: Nat) -> String:
  +tt = {t : Nat}
  +a = {Nat.sub(U32.to_nat(be), 150n) : Nat}
  +b = {Nat.sub(150n, U32.to_nat(be)) : Nat}
  +even = {U32.is_zero(U32.and(f, 1)) : Bool}
  Short.finite.fin(even, Short.fix(even,
    St{Big.shl(Nat.add(Nat.add(a, 1n), tt), Big.of(f)),
      Big.shl(Nat.add(Nat.add(b, 1n), tt), Big.of(1)),
      Big.shl(Nat.add(a, tt), Big.of(1)), Big.shl(a, Big.of(1))}))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Big.of
  https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Big.shl
  https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.finite.fin
  https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.fix
  https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=St