~/jendhub

def rank_exact

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

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

131def rank_exact(+shape: Shape.Shape) -> {U32.to_nat(Shape.rank(shape)) == Shape.rank_dimensions(Shape.dimensions(shape)) : Nat}:
132  match shape:
133    case Shape.SShape{+dims, size, exact, +rank_bound, capacity_bound}:
134      Conversion.natural_word_exact(Shape.rank_dimensions(dims), 4,
135        Equal.sym(Bool, True{}, Nat.is_le(Shape.rank_dimensions(dims), 4n), Nats.le_true(Shape.rank_dimensions(dims), 4n, rank_bound)))

Uses (11)

Used by (4)