def rows_of

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_LAWS.bend:316

import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend as BatchedMatmulLAWS
import Base

316# The extent before the last: the rows of a matrix.
317def rows_of(dims: List<&2, Nat>) -> Nat:
318  match dims:
319    case +x <> +y <> Nil{}:
320      x
321    case +x <> +y <> +z <> tail:
322      rows_of(y <> z <> tail)
323    case rest:
324      0n

Uses (2)

Used by (1)