WordConversion.capacity_within: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion
Lines 579-583 of bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&start_line=579&end_line=583

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as NatProof

def capacity_within(+number: Nat, within: Shape.LE(number, 1048576n)) ->
  {Nat.is_le(number, U32.to_nat(1048576)) == True{} : Bool}:
  Equal.trans(Bool, Nat.is_le(number, U32.to_nat(1048576)), Nat.is_le(number, 1048576n), True{},
    Equal.cong(Nat, Bool, n => Nat.is_le(number, n), U32.to_nat(1048576), 1048576n, capacity_word_nat()),
    Equal.sym(Bool, True{}, Nat.is_le(number, 1048576n), NatProof.le_true(number, 1048576n, within)))

Uses (10):
  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=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LE
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=le_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=capacity_word_nat