def word_length

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

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

3047def word_length(+items: List<&2, U32>) -> {List.length(&2, U32, items) == Shape.rank_dimensions(items) : Nat}:
3048  match items:
3049    case Nil{}:
3050      {==}
3051    case head <> +tail:
3052      Equal.cong(Nat, Nat, n => 1n+n, List.length(&2, U32, tail), Shape.rank_dimensions(tail), word_length(tail))