~/jendhub

def cursor_bound

bendtorch-core@0.1.0.0 · src/tensor/axis_algebra.bend:150

import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as AxisAlgebra
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

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

Uses (5)

Used by (1)