def words_valid_rank

bendtorch-core@0.1.0.0 · src/tensor/permutation_mapping.bend:404

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

404def words_valid_rank(+dimensions: List<&2, U32>, +values: List<&2, U32>, valid: Layout.WordsValid(dimensions, values)) ->
405  {Shape.rank_dimensions(values) == Shape.rank_dimensions(dimensions) : Nat}:
406  match dimensions values:
407    case Nil{} Nil{}:
408      {==}
409    case +dimension <> +dt +value <> +vt:
410      Layout.WStep{bound, tail} = valid
411      Equal.cong(Nat, Nat, n => 1n+n, Shape.rank_dimensions(vt), Shape.rank_dimensions(dt), words_valid_rank(dt, vt, tail))
412    case Nil{} head <> tail:
413      match valid:
414    case head <> tail Nil{}:
415      match valid: