AxisAlgebra.cursor_bound: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as AxisAlgebra
Lines 150-153 of bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&start_line=150&end_line=153

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 Nats

def cursor_bound(+rank: Nat, +cursor: Nat, bound: Shape.LE(Nat.add(rank, cursor), 4n)) -> Shape.LE(cursor, 4n):
  Nats.le_add_left(cursor, rank, 4n,
    %add_comm(rank, cursor) : Shape.LE(_, 4n)
    bound)

Uses (5):
  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=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_add_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=add_comm